1 /-
2 Copyright (c) 2017 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro, Johannes Hölzl
5
6 Ordered monoids and groups.
7 -/
8 import algebra.group order.bounded_lattice tactic.basic
src └───────────┘ └───────────────────┘ └──────────┘
9
10 universe u
11 variable {α : Type u}
12
13 section old_structure_cmd
14
15 set_option old_structure_cmd true
doc └───────────────┘
16 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
17 /-- An ordered (additive) commutative monoid is a commutative monoid
18 with a partial order such that addition is an order embedding, i.e.
19 `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
20 class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
id ┴ └───┘ └─────────────┘ ┴ └───────────┘ ┴
src └─────────────┘ └───────────┘
typ ┴ └───┘ └─────────────┘ ┴ └───────────┘ ┴
21 (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
22 (lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
23
24 /-- A canonically ordered monoid is an ordered commutative monoid
25 in which the ordering coincides with the divisibility relation,
26 which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
27 This is satisfied by the natural numbers, for example, but not
28 the integers or other ordered groups. -/
29 class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, lattice.order_bot α :=
id ┴ └───┘ └─────────────────┘ ┴ └───────────────┘ ┴
src └─────────────────┘ └───────────────┘
typ ┴ └───┘ └─────────────────┘ ┴ └───────────────┘ ┴
doc └─────────────────┘ └───────────────┘
30 (le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
31
32 end old_structure_cmd
33
34 section ordered_comm_monoid
35 variables [ordered_comm_monoid α] {a b c d : α}
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
36
37 lemma add_le_add_left' (h : a ≤ b) : c + a ≤ c + b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
38 ordered_comm_monoid.add_le_add_left a b h c
id └─────────────────────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────────────────────┘
typ └─────────────────────────────────┘ ┴ ┴ ┴ ┴
39
40 lemma add_le_add_right' (h : a ≤ b) : a + c ≤ b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
41 add_comm c a ▸ add_comm c b ▸ add_le_add_left' h
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────────────┘ ┴
src └──────┘ ┴ └──────┘ ┴ └──────────────┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────────────┘ ┴
42
43 lemma lt_of_add_lt_add_left' : a + b < a + c → b < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
44 ordered_comm_monoid.lt_of_add_lt_add_left a b c
id └───────────────────────────────────────┘ ┴ ┴ ┴
src └───────────────────────────────────────┘
typ └───────────────────────────────────────┘ ┴ ┴ ┴
45
46 lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
47 le_trans (add_le_add_right' h₁) (add_le_add_left' h₂)
id └──────┘ └───────────────┘ └┘ └──────────────┘ └┘
src └──────┘ └───────────────┘ └──────────────┘
typ └──────┘ └───────────────┘ └┘ └──────────────┘ └┘
48
49 lemma le_add_of_nonneg_right' (h : 0 ≤ b) : a ≤ a + b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
50 have a + b ≥ a + 0, from add_le_add_left' h,
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴
src ┴ ┴ ┴ └──────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴
51 by rwa add_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
52
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
53 lemma le_add_of_nonneg_left' (h : 0 ≤ b) : a ≤ b + a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
54 have 0 + a ≤ b + a, from add_le_add_right' h,
id ┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴
src ┴ ┴ ┴ └───────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴
55 by rwa zero_add at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
56
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
57 lemma lt_of_add_lt_add_right' (h : a + b < c + b) : a < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
58 lt_of_add_lt_add_left'
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
59 (show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src ┴ ┴ ┴ └──┘└──────┘┴ ┴ └┘└──────┘┴ ┴ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└──────┘┴┴┴┴└┘└──────┘┴┴┴┴┴ └─────────┘
doc └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────────┘
txt └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────────┘
par └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────────┘
pid └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st └────────────────────┘└────────────┘└────────────┘└─┘
60
61 -- here we start using properties of zero.
62 lemma le_add_of_nonneg_of_le' (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
63 zero_add b ▸ add_le_add' ha hbc
id └──────┘ ┴ ┴ └─────────┘ └┘ └─┘
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ └─────────┘ └┘ └─┘
64
65 lemma le_add_of_le_of_nonneg' (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
66 add_zero b ▸ add_le_add' hbc ha
id └──────┘ ┴ ┴ └─────────┘ └─┘ └┘
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ └─────────┘ └─┘ └┘
67
68 lemma add_nonneg' (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
69 le_add_of_nonneg_of_le' ha hb
id └─────────────────────┘ └┘ └┘
src └─────────────────────┘
typ └─────────────────────┘ └┘ └┘
70
71 lemma add_pos_of_pos_of_nonneg' (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
72 lt_of_lt_of_le ha $ le_add_of_nonneg_right' hb
id └────────────┘ └┘ └─────────────────────┘ └┘
src └────────────┘ └─────────────────────┘
typ └────────────┘ └┘ └─────────────────────┘ └┘
73
74 lemma add_pos' (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
75 add_pos_of_pos_of_nonneg' ha $ le_of_lt hb
id └───────────────────────┘ └┘ └──────┘ └┘
src └───────────────────────┘ └──────┘
typ └───────────────────────┘ └┘ └──────┘ └┘
76
77 lemma add_pos_of_nonneg_of_pos' (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
78 lt_of_lt_of_le hb $ le_add_of_nonneg_left' ha
id └────────────┘ └┘ └────────────────────┘ └┘
src └────────────┘ └────────────────────┘
typ └────────────┘ └┘ └────────────────────┘ └┘
79
80 lemma add_nonpos' (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
81 zero_add (0:α) ▸ (add_le_add' ha hb)
id └──────┘ ┴ ┴ └─────────┘ └┘ └┘
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ └─────────┘ └┘ └┘
82
83 lemma add_le_of_nonpos_of_le' (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
84 zero_add c ▸ add_le_add' ha hbc
id └──────┘ ┴ ┴ └─────────┘ └┘ └─┘
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ └─────────┘ └┘ └─┘
85
86 lemma add_le_of_le_of_nonpos' (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
87 add_zero c ▸ add_le_add' hbc ha
id └──────┘ ┴ ┴ └─────────┘ └─┘ └┘
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ └─────────┘ └─┘ └┘
88
89 lemma add_neg_of_neg_of_nonpos' (ha : a < 0) (hb : b ≤ 0) : a + b < 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
90 lt_of_le_of_lt (add_le_of_le_of_nonpos' (le_refl _) hb) ha
id └────────────┘ └─────────────────────┘ └─────┘ └┘ └┘
src └────────────┘ └─────────────────────┘ └─────┘
typ └────────────┘ └─────────────────────┘ └─────┘ └┘ └┘
91
92 lemma add_neg_of_nonpos_of_neg' (ha : a ≤ 0) (hb : b < 0) : a + b < 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
93 lt_of_le_of_lt (add_le_of_nonpos_of_le' ha (le_refl _)) hb
id └────────────┘ └─────────────────────┘ └┘ └─────┘ └┘
src └────────────┘ └─────────────────────┘ └─────┘
typ └────────────┘ └─────────────────────┘ └┘ └─────┘ └┘
94
95 lemma add_neg' (ha : a < 0) (hb : b < 0) : a + b < 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
96 add_neg_of_nonpos_of_neg' (le_of_lt ha) hb
id └───────────────────────┘ └──────┘ └┘ └┘
src └───────────────────────┘ └──────┘
typ └───────────────────────┘ └──────┘ └┘ └┘
97
98 lemma lt_add_of_nonneg_of_lt' (ha : 0 ≤ a) (hbc : b < c) : b < a + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
99 lt_of_lt_of_le hbc $ le_add_of_nonneg_left' ha
id └────────────┘ └─┘ └────────────────────┘ └┘
src └────────────┘ └────────────────────┘
typ └────────────┘ └─┘ └────────────────────┘ └┘
100
101 lemma lt_add_of_lt_of_nonneg' (hbc : b < c) (ha : 0 ≤ a) : b < c + a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
102 lt_of_lt_of_le hbc $ le_add_of_nonneg_right' ha
id └────────────┘ └─┘ └─────────────────────┘ └┘
src └────────────┘ └─────────────────────┘
typ └────────────┘ └─┘ └─────────────────────┘ └┘
103
104 lemma lt_add_of_pos_of_lt' (ha : 0 < a) (hbc : b < c) : b < a + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴
105 lt_add_of_nonneg_of_lt' (le_of_lt ha) hbc
id └─────────────────────┘ └──────┘ └┘ └─┘
src └─────────────────────┘ └──────┘
typ └─────────────────────┘ └──────┘ └┘ └─┘
106
107 lemma lt_add_of_lt_of_pos' (hbc : b < c) (ha : 0 < a) : b < c + a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
108 lt_add_of_lt_of_nonneg' hbc (le_of_lt ha)
id └─────────────────────┘ └─┘ └──────┘ └┘
src └─────────────────────┘ └──────┘
typ └─────────────────────┘ └─┘ └──────┘ └┘
109
110 lemma add_lt_of_nonpos_of_lt' (ha : a ≤ 0) (hbc : b < c) : a + b < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
111 lt_of_le_of_lt (add_le_of_nonpos_of_le' ha (le_refl _)) hbc
id └────────────┘ └─────────────────────┘ └┘ └─────┘ └─┘
src └────────────┘ └─────────────────────┘ └─────┘
typ └────────────┘ └─────────────────────┘ └┘ └─────┘ └─┘
112
113 lemma add_lt_of_lt_of_nonpos' (hbc : b < c) (ha : a ≤ 0) : b + a < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
114 lt_of_le_of_lt (add_le_of_le_of_nonpos' (le_refl _) ha) hbc
id └────────────┘ └─────────────────────┘ └─────┘ └┘ └─┘
src └────────────┘ └─────────────────────┘ └─────┘
typ └────────────┘ └─────────────────────┘ └─────┘ └┘ └─┘
115
116 lemma add_lt_of_neg_of_lt' (ha : a < 0) (hbc : b < c) : a + b < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
117 add_lt_of_nonpos_of_lt' (le_of_lt ha) hbc
id └─────────────────────┘ └──────┘ └┘ └─┘
src └─────────────────────┘ └──────┘
typ └─────────────────────┘ └──────┘ └┘ └─┘
118
119 lemma add_lt_of_lt_of_neg' (hbc : b < c) (ha : a < 0) : b + a < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
120 add_lt_of_lt_of_nonpos' hbc (le_of_lt ha)
id └─────────────────────┘ └─┘ └──────┘ └┘
src └─────────────────────┘ └──────┘
typ └─────────────────────┘ └─┘ └──────┘ └┘
121
122 lemma add_eq_zero_iff' (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
123 iff.intro
id └───────┘
src └───────┘
typ └───────┘
124 (assume hab : a + b = 0,
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
125 have a ≤ 0, from hab ▸ le_add_of_le_of_nonneg' (le_refl _) hb,
id ┴ ┴ └─┘ ┴ └─────────────────────┘ └─────┘ └┘
src ┴ ┴ └─────────────────────┘ └─────┘
typ ┴ ┴ └─┘ ┴ └─────────────────────┘ └─────┘ └┘
126 have a = 0, from le_antisymm this ha,
id ┴ ┴ └─────────┘ └──┘ └┘
src ┴ └─────────┘
typ ┴ ┴ └─────────┘ └──┘ └┘
127 have b ≤ 0, from hab ▸ le_add_of_nonneg_of_le' ha (le_refl _),
id ┴ ┴ └─┘ ┴ └─────────────────────┘ └┘ └─────┘
src ┴ ┴ └─────────────────────┘ └─────┘
typ ┴ ┴ └─┘ ┴ └─────────────────────┘ └┘ └─────┘
128 have b = 0, from le_antisymm this hb,
id ┴ ┴ └─────────┘ └──┘ └┘
src ┴ └─────────┘
typ ┴ ┴ └─────────┘ └──┘ └┘
129 and.intro ‹a = 0› ‹b = 0›)
id └───────┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
130 (assume ⟨ha', hb'⟩, by rw [ha', hb', add_zero])
id ┴ └─┘ └─┘ └──────┘
src └──┘ └┘ └┘└──────┘┴
typ ┴ └──┘└─┘└┘└─┘└┘└──────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └──────┘└───┘└────────┘┴
131
132 lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
id ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ └──┘ ┴
133 add_pos' h h
id └──────┘ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴
134
135 end ordered_comm_monoid
136
137 namespace units
138
139 instance [monoid α] [i : preorder α] : preorder (units α) :=
id └────┘ ┴ └──────┘ ┴ └──────┘ └───┘ ┴
src └────┘ └──────┘ └──────┘ └───┘
typ └────┘ ┴ └──────┘ ┴ └──────┘ └───┘ ┴
140 preorder.lift (coe : units α → α) i
id └───────────┘ └─┘ └───┘ ┴ ┴ ┴
src └───────────┘ └─┘ └───┘
typ └───────────┘ └─┘ └───┘ ┴ ┴ ┴
141
142 @[simp] theorem coe_le_coe [monoid α] [preorder α] {a b : units α} :
id └────┘ ┴ └──────┘ ┴ └───┘ ┴
src └────┘ └──────┘ └───┘
typ └────┘ ┴ └──────┘ ┴ └───┘ ┴
doc └──┘
143 (a : α) ≤ b ↔ a ≤ b := iff.rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
144
145 @[simp] theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} :
id └────┘ ┴ └──────┘ ┴ └───┘ ┴
src └────┘ └──────┘ └───┘
typ └────┘ ┴ └──────┘ ┴ └───┘ ┴
doc └──┘
146 (a : α) < b ↔ a < b := iff.rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
147
148 instance [monoid α] [i : partial_order α] : partial_order (units α) :=
id └────┘ ┴ └───────────┘ ┴ └───────────┘ └───┘ ┴
src └────┘ └───────────┘ └───────────┘ └───┘
typ └────┘ ┴ └───────────┘ ┴ └───────────┘ └───┘ ┴
149 partial_order.lift (coe : units α → α) (by ext) i
id └────────────────┘ └─┘ └───┘ ┴ ┴ ┴
src └────────────────┘ └─┘ └───┘ └─┘
typ └────────────────┘ └─┘ └───┘ ┴ ┴ └─┘ ┴
doc └─┘
txt └─┘
par └─┘
st └──┘
150
151 instance [monoid α] [i : linear_order α] : linear_order (units α) :=
id └────┘ ┴ └──────────┘ ┴ └──────────┘ └───┘ ┴
src └────┘ └──────────┘ └──────────┘ └───┘
typ └────┘ ┴ └──────────┘ ┴ └──────────┘ └───┘ ┴
152 linear_order.lift (coe : units α → α) (by ext) i
id └───────────────┘ └─┘ └───┘ ┴ ┴ ┴
src └───────────────┘ └─┘ └───┘ └─┘
typ └───────────────┘ └─┘ └───┘ ┴ ┴ └─┘ ┴
doc └─┘
txt └─┘
par └─┘
st └──┘
153
154 instance [monoid α] [i : decidable_linear_order α] : decidable_linear_order (units α) :=
id └────┘ ┴ └────────────────────┘ ┴ └────────────────────┘ └───┘ ┴
src └────┘ └────────────────────┘ └────────────────────┘ └───┘
typ └────┘ ┴ └────────────────────┘ ┴ └────────────────────┘ └───┘ ┴
155 decidable_linear_order.lift (coe : units α → α) (by ext) i
id └─────────────────────────┘ └─┘ └───┘ ┴ ┴ ┴
src └─────────────────────────┘ └─┘ └───┘ └─┘
typ └─────────────────────────┘ └─┘ └───┘ ┴ ┴ └─┘ ┴
doc └─┘
txt └─┘
par └─┘
st └──┘
156
157 theorem max_coe [monoid α] [decidable_linear_order α] {a b : units α} :
id └────┘ ┴ └────────────────────┘ ┴ └───┘ ┴
src └────┘ └────────────────────┘ └───┘
typ └────┘ ┴ └────────────────────┘ ┴ └───┘ ┴
158 (↑(max a b) : α) = max a b :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
159 by by_cases a ≤ b; simp [max, h]
id ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴┴┴ └────┘└─┘└┘ └─
typ └───────┘┴┴┴┴┴ └────┘└─┘└┘┴└─
doc └───────┘ ┴ ┴ └────┘ └┘ └─
txt └───────┘ ┴ ┴ └────┘ └┘ └─
par └───────┘ ┴ ┴ └────┘ └┘ └─
pid ┴ ┴ ┴ ┴┴ └┘ ┴└
st └──────────────────────────────
160
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
161 theorem min_coe [monoid α] [decidable_linear_order α] {a b : units α} :
id └────┘ ┴ └────────────────────┘ ┴ └───┘ ┴
src └────┘ └────────────────────┘ └───┘
typ └────┘ ┴ └────────────────────┘ ┴ └───┘ ┴
162 (↑(min a b) : α) = min a b :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
163 by by_cases a ≤ b; simp [min, h]
id ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴┴┴ └────┘└─┘└┘ └─
typ └───────┘┴┴┴┴┴ └────┘└─┘└┘┴└─
doc └───────┘ ┴ ┴ └────┘ └┘ └─
txt └───────┘ ┴ ┴ └────┘ └┘ └─
par └───────┘ ┴ ┴ └────┘ └┘ └─
pid ┴ ┴ ┴ ┴┴ └┘ ┴└
st └──────────────────────────────
164
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
165 end units
166
167 namespace with_zero
168 open lattice
169
170 instance [preorder α] : preorder (with_zero α) := with_bot.preorder
id └──────┘ ┴ └──────┘ └───────┘ ┴ └───────────────┘
src └──────┘ └──────┘ └───────┘ └───────────────┘
typ └──────┘ ┴ └──────┘ └───────┘ ┴ └───────────────┘
171 instance [partial_order α] : partial_order (with_zero α) := with_bot.partial_order
id └───────────┘ ┴ └───────────┘ └───────┘ ┴ └────────────────────┘
src └───────────┘ └───────────┘ └───────┘ └────────────────────┘
typ └───────────┘ ┴ └───────────┘ └───────┘ ┴ └────────────────────┘
172 instance [partial_order α] : order_bot (with_zero α) := with_bot.order_bot
id └───────────┘ ┴ └───────┘ └───────┘ ┴ └────────────────┘
src └───────────┘ └───────┘ └───────┘ └────────────────┘
typ └───────────┘ ┴ └───────┘ └───────┘ ┴ └────────────────┘
doc └───────┘
173 instance [lattice α] : lattice (with_zero α) := with_bot.lattice
id └─────┘ ┴ └─────┘ └───────┘ ┴ └──────────────┘
src └─────┘ └─────┘ └───────┘ └──────────────┘
typ └─────┘ ┴ └─────┘ └───────┘ ┴ └──────────────┘
doc └─────┘ └─────┘
174 instance [linear_order α] : linear_order (with_zero α) := with_bot.linear_order
id └──────────┘ ┴ └──────────┘ └───────┘ ┴ └───────────────────┘
src └──────────┘ └──────────┘ └───────┘ └───────────────────┘
typ └──────────┘ ┴ └──────────┘ └───────┘ ┴ └───────────────────┘
175 instance [decidable_linear_order α] :
id └────────────────────┘ ┴
src └────────────────────┘
typ └────────────────────┘ ┴
176 decidable_linear_order (with_zero α) := with_bot.decidable_linear_order
id └────────────────────┘ └───────┘ ┴ └─────────────────────────────┘
src └────────────────────┘ └───────┘ └─────────────────────────────┘
typ └────────────────────┘ └───────┘ ┴ └─────────────────────────────┘
177
178 def ordered_comm_monoid [ordered_comm_monoid α]
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
doc └─────────────────┘
179 (zero_le : ∀ a : α, 0 ≤ a) : ordered_comm_monoid (with_zero α) :=
id ┴ ┴ ┴ └─────────────────┘ └───────┘ ┴
src ┴ └─────────────────┘ └───────┘
typ ┴ ┴ ┴ └─────────────────┘ └───────┘ ┴
doc └─────────────────┘
180 begin
st └─────
181 suffices, refine {
src └──────┘ └─────┘ └
typ └──────┘ └─────┘ └
doc └──────┘ └─────┘ └
txt └──────┘ └─────┘ └
par └──────┘ └─────┘ └
pid └──────┘ ┴ └
st ─────────┘└──────────
182 add_le_add_left := this,
id └──┘
src ──────────────────────┘ └─
typ ──────────────────────┘└──┘└─
doc ──────────────────────┘ └─
txt ──────────────────────┘ └─
par ──────────────────────┘ └─
pid ──────────────────────┘ └─
st ─────────────────────────────
183 ..with_zero.partial_order,
id └─────────────────────┘
src ─────┘└─────────────────────┘└─
typ ─────┘└─────────────────────┘└─
doc ─────┘ └─
txt ─────┘ └─
par ─────┘ └─
pid ─────┘ └─
st ───────────────────────────────
184 ..with_zero.add_comm_monoid, .. },
id └───────────────────────┘
src ─────┘└───────────────────────┘└────┘
typ ─────┘└───────────────────────┘└────┘
doc ─────┘ └────┘
txt ─────┘ └────┘
par ─────┘ └────┘
pid ─────┘ └────┘
st ────────────────────────────────────┘└─
185 { intros a b c h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
186 have h' := lt_iff_le_not_le.1 h,
id └──────────────┘ ┴
src └─────────┘└──────────────┘└─┘
typ └─────────┘└──────────────┘└─┘┴
doc └─────────┘ └─┘
txt └─────────┘ └─┘
par └─────────┘ └─┘
pid └─────┘┴└─┘ └─┘
st ──────────────────────────────────┘└─
187 rw lt_iff_le_not_le at ⊢,
id └──────────────┘
src └─┘└──────────────┘└───┘
typ └─┘└──────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────────────────┘└─
188 refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
id └┘ └──┘
src └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
typ └─────┘ └────────┘ └───┘└┘└─┘ ┴└──┘└───┘ └─┘
doc └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
txt └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
par └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
pid ┴ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
st ─────────────────────────────────────────────────┘└─
189 cases h₂, cases c with c,
id └┘ ┴
src └────┘ └────┘ └─────┘
typ └────┘└┘ └────┘┴└─────┘
doc └────┘ └────┘ └─────┘
txt └────┘ └────┘ └─────┘
par └────┘ └────┘ └─────┘
pid ┴ ┴ └─────┘
st ───────────┘└──────────────┘└─
190 { cases h'.2 (this _ _ bot_le a) },
id └┘ └──┘ └────┘ ┴
src └────┘ └─┘ └───┘└────┘┴ └┘
typ └────┘└┘└─┘ └──┘└───┘└────┘┴┴└┘
doc └────┘ └─┘ └───┘ ┴ └┘
txt └────┘ └─┘ └───┘ ┴ └┘
par └────┘ └─┘ └───┘ ┴ └┘
pid ┴ └─┘ └───┘ ┴ ┴┴
st ─────┘└─────────────────────────────┘└┘└
191 { refine ⟨_, rfl, _⟩,
id └─┘
src └─────┘ └─┘└─┘└──┘
typ └─────┘ └─┘└─┘└──┘
doc └─────┘ └─┘ └──┘
txt └─────┘ └─┘ └──┘
par └─────┘ └─┘ └──┘
pid ┴ └─┘ └──┘
st ───────────────────────┘└─
192 cases a with a,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ───────────────────┘└─
193 { exact with_bot.some_le_some.1 h'.1 },
id └───────────────────┘ └┘
src └────┘└───────────────────┘└─┘ └─┘
typ └────┘└───────────────────┘└─┘└┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st ───────┘└─────────────────────────────────┘└┘└
194 { exact le_of_lt (lt_of_add_lt_add_left' $
id └──────┘ └────────────────────┘
src └────┘└──────┘┴ └────────────────────┘┴ └
typ └────┘└──────┘┴ └────────────────────┘┴ └
doc └────┘ ┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────────────────────────────────────
195 with_bot.some_lt_some.1 h), } } },
id └───────────────────┘ ┴
src ─────────┘└───────────────────┘└─┘ ┴
typ ─────────┘└───────────────────┘└─┘┴┴
doc ─────────┘ └─┘ ┴
txt ─────────┘ └─┘ ┴
par ─────────┘ └─┘ ┴
pid ─────────┘ └─┘ ┴
st ───────────────────────────────────┘└──────┘└
196 { intros a b h c ca h₂,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ───────────────────────┘└─
197 cases b with b,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
198 { rw le_antisymm h bot_le at h₂,
id └─────────┘ ┴ └────┘
src └─┘└─────────┘┴ ┴└────┘└────┘
typ └─┘└─────────┘┴┴┴└────┘└────┘
doc └─┘ ┴ ┴ └────┘
txt └─┘ ┴ ┴ └────┘
par └─┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └────┘
st ─────┘└───────────────────────────┘└─
199 exact ⟨_, h₂, le_refl _⟩ },
id └┘ └─────┘
src └────┘ └─┘ └┘└─────┘└──┘
typ └────┘ └─┘└┘└┘└─────┘└──┘
doc └────┘ └─┘ └┘ └──┘
txt └────┘ └─┘ └┘ └──┘
par └────┘ └─┘ └┘ └──┘
pid ┴ └─┘ └┘ └─┘┴
st ──────────────────────────────┘└┘└
200 cases a with a,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
201 { change c + 0 = some ca at h₂,
id ┴ ┴ ┴ └──┘ └┘
src └─────┘ ┴┴└─┘┴┴└──┘┴ └────┘
typ └─────┘┴┴┴└─┘┴┴└──┘┴└┘└────┘
doc └─────┘ ┴ └─┘ ┴ ┴ └────┘
txt └─────┘ ┴ └─┘ ┴ ┴ └────┘
par └─────┘ ┴ └─┘ ┴ ┴ └────┘
pid ┴ ┴ └─┘ ┴ ┴ ┴└───┘
st ─────┘└──────────────────────────┘└─
202 simp at h₂, simp [h₂],
id └┘
src └────────┘ └────┘ ┴
typ └────────┘ └────┘└┘┴
doc └────────┘ └────┘ ┴
txt └────────┘ └────┘ ┴
par └────────┘ └────┘ ┴
pid ┴└───┘ ┴┴ ┴
st ───────────────┘└─────────┘└─
203 exact ⟨_, rfl, by simpa using add_le_add_left' (zero_le b)⟩ },
id └─┘ └──────────────┘ └─────┘ ┴
src └────┘ └─┘└─┘└┘ ┴└──────────┘└──────────────┘┴ ┴ ┴└┘
typ └────┘ └─┘└─┘└┘ ┴└──────────┘└──────────────┘┴ └─────┘┴┴┴└┘
doc └────┘ └─┘ └┘ ┴└──────────┘ ┴ ┴ ┴└┘
txt └────┘ └─┘ └┘ ┴└──────────┘ ┴ ┴ ┴└┘
par └────┘ └─┘ └┘ ┴└──────────┘ ┴ ┴ ┴└┘
pid ┴ └─┘ └┘ └───────────┘ ┴ ┴ └┘┴
st ──────────────────────┘└───────────────────────────────────────┘└┘└┘└
204 { simp at h,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└──┘
st ──────────────┘└─
205 cases c with c; change some _ = _ at h₂;
id ┴ └──┘
src └────┘ └─────┘ └─────┘└──┘└─┘ └──────┘
typ └────┘┴└─────┘ └─────┘└──┘└─┘ └──────┘
doc └────┘ └─────┘ └─────┘ └─┘ └──────┘
txt └────┘ └─────┘ └─────┘ └─┘ └──────┘
par └────┘ └─────┘ └─────┘ └─┘ └──────┘
pid ┴ └─────┘ ┴ └─┘ └┘┴└───┘
st ───────────────────────────────────────────────
206 simp [-add_comm] at h₂; subst ca; refine ⟨_, rfl, _⟩,
id └┘ └─┘
src └────────────────────┘ └────┘ └─────┘ └─┘└─┘└──┘
typ └────────────────────┘ └────┘└┘ └─────┘ └─┘└─┘└──┘
doc └────────────────────┘ └────┘ └─────┘ └─┘ └──┘
txt └────────────────────┘ └────┘ └─────┘ └─┘ └──┘
par └────────────────────┘ └────┘ └─────┘ └─┘ └──┘
pid ┴└─────────┘┴└───┘ ┴ ┴ └─┘ └──┘
st ───────────────────────────────────────────────────────────┘└─
207 { exact h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────┘└──────┘└┘└
208 { exact add_le_add_left' h } } }
id └──────────────┘ ┴
src └────┘└──────────────┘┴ ┴
typ └────┘└──────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────┘└─────
209 end
st ──┘
210
211 end with_zero
212
213 namespace with_top
214 open lattice
215
216 instance [add_semigroup α] : add_semigroup (with_top α) :=
id └───────────┘ ┴ └───────────┘ └──────┘ ┴
src └───────────┘ └───────────┘ └──────┘
typ └───────────┘ ┴ └───────────┘ └──────┘ ┴
217 { add := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b)),
id └┘ └┘ └┘└───┘ ┴ └┘└──┘ ┴ ┴ ┴ ┴
src └───┘ └──┘ ┴
typ └┘ └┘ └┘└───┘ ┴ └┘└──┘ ┴ ┴ ┴ ┴
218 ..@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _ }
id └────────────────────┘ └─────────────────┘ └────────────┘ ┴
src └────────────────────┘ └─────────────────┘ └────────────┘
typ └────────────────────┘ └─────────────────┘ └────────────┘ ┴
219
220 lemma coe_add [add_semigroup α] {a b : α} : ((a + b : α) : with_top α) = a + b := rfl
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └───────────┘ ┴ └──────┘ ┴ ┴ └─┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └─┘
221
222 instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
id └────────────────┘ ┴ └────────────────┘ └──────┘ ┴
src └────────────────┘ └────────────────┘ └──────┘
typ └────────────────┘ ┴ └────────────────┘ └──────┘ ┴
223 { ..@additive.add_comm_semigroup _ $
id └─────────────────────────┘
src └─────────────────────────┘
typ └─────────────────────────┘
224 @with_zero.comm_semigroup (multiplicative α) _ }
id └──────────────────────┘ └────────────┘ ┴
src └──────────────────────┘ └────────────┘
typ └──────────────────────┘ └────────────┘ ┴
225
226 instance [add_monoid α] : add_monoid (with_top α) :=
id └────────┘ ┴ └────────┘ └──────┘ ┴
src └────────┘ └────────┘ └──────┘
typ └────────┘ ┴ └────────┘ └──────┘ ┴
227 { zero := some 0,
id └──┘
src └──┘
typ └──┘
228 add := (+),
id ┴
src ┴
typ ┴
229 ..@additive.add_monoid _ $ @with_zero.monoid (multiplicative α) _ }
id └─────────────────┘ └──────────────┘ └────────────┘ ┴
src └─────────────────┘ └──────────────┘ └────────────┘
typ └─────────────────┘ └──────────────┘ └────────────┘ ┴
230
231 instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
id └─────────────┘ ┴ └─────────────┘ └──────┘ ┴
src └─────────────┘ └─────────────┘ └──────┘
typ └─────────────┘ ┴ └─────────────┘ └──────┘ ┴
232 { zero := 0,
233 add := (+),
id ┴
src ┴
typ ┴
234 ..@additive.add_comm_monoid _ $
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
235 @with_zero.comm_monoid (multiplicative α) _ }
id └───────────────────┘ └────────────┘ ┴
src └───────────────────┘ └────────────┘
typ └───────────────────┘ └────────────┘ ┴
236
237 instance [ordered_comm_monoid α] : ordered_comm_monoid (with_top α) :=
id └─────────────────┘ ┴ └─────────────────┘ └──────┘ ┴
src └─────────────────┘ └─────────────────┘ └──────┘
typ └─────────────────┘ ┴ └─────────────────┘ └──────┘ ┴
doc └─────────────────┘ └─────────────────┘
238 begin
st └─────
239 suffices, refine {
src └──────┘ └─────┘ └
typ └──────┘ └─────┘ └
doc └──────┘ └─────┘ └
txt └──────┘ └─────┘ └
par └──────┘ └─────┘ └
pid └──────┘ ┴ └
st ─────────┘└──────────
240 add_le_add_left := this,
id └──┘
src ──────────────────────┘ └─
typ ──────────────────────┘└──┘└─
doc ──────────────────────┘ └─
txt ──────────────────────┘ └─
par ──────────────────────┘ └─
pid ──────────────────────┘ └─
st ─────────────────────────────
241 ..with_top.partial_order,
id └────────────────────┘
src ─────┘└────────────────────┘└─
typ ─────┘└────────────────────┘└─
doc ─────┘ └─
txt ─────┘ └─
par ─────┘ └─
pid ─────┘ └─
st ──────────────────────────────
242 ..with_top.add_comm_monoid, ..},
id └──────────────────────┘
src ─────┘└──────────────────────┘└───┘
typ ─────┘└──────────────────────┘└───┘
doc ─────┘ └───┘
txt ─────┘ └───┘
par ─────┘ └───┘
pid ─────┘ └───┘
st ──────────────────────────────────┘└─
243 { intros a b c h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
244 have h' := h,
id ┴
src └─────────┘
typ └─────────┘┴
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────┘┴└─┘
st ───────────────┘└─
245 rw lt_iff_le_not_le at h' ⊢,
id └──────────────┘
src └─┘└──────────────┘└──────┘
typ └─┘└──────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ──────────────────────────────┘└─
246 refine ⟨λ c h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
id └┘ └──┘
src └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
typ └─────┘ └────────┘ └───┘└┘└─┘ ┴└──┘└───┘ └─┘
doc └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
txt └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
par └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
pid ┴ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
st ─────────────────────────────────────────────────┘└─
247 cases h₂, cases a with a,
id └┘ ┴
src └────┘ └────┘ └─────┘
typ └────┘└┘ └────┘┴└─────┘
doc └────┘ └────┘ └─────┘
txt └────┘ └────┘ └─────┘
par └────┘ └────┘ └─────┘
pid ┴ ┴ └─────┘
st ───────────┘└──────────────┘└─
248 { exact (not_le_of_lt h).elim le_top },
id └──────────┘ ┴ └────┘
src └────┘ └──────────┘┴ └─────┘└────┘┴
typ └────┘ └──────────┘┴┴└─────┘└────┘┴
doc └────┘ ┴ └─────┘ ┴
txt └────┘ ┴ └─────┘ ┴
par └────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ─────┘└─────────────────────────────────┘└┘└
249 cases b with b,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
250 { exact (not_le_of_lt h).elim le_top },
id └──────────┘ ┴ └────┘
src └────┘ └──────────┘┴ └─────┘└────┘┴
typ └────┘ └──────────┘┴┴└─────┘└────┘┴
doc └────┘ ┴ └─────┘ ┴
txt └────┘ ┴ └─────┘ ┴
par └────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ─────┘└─────────────────────────────────┘└┘└
251 { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left' $
id └─┘ └──────┘ └────────────────────┘
src └────┘ └─┘└─┘└┘└──────┘┴ └────────────────────┘┴ └
typ └────┘ └─┘└─┘└┘└──────┘┴ └────────────────────┘┴ └
doc └────┘ └─┘ └┘ ┴ ┴ └
txt └────┘ └─┘ └┘ ┴ ┴ └
par └────┘ └─┘ └┘ ┴ ┴ └
pid ┴ └─┘ └┘ ┴ ┴ └
st ────────────────────────────────────────────────────────
252 with_top.some_lt_some.1 h)⟩ } },
id └───────────────────┘ ┴
src ───────┘└───────────────────┘└─┘ └─┘
typ ───────┘└───────────────────┘└─┘┴└─┘
doc ───────┘ └─┘ └─┘
txt ───────┘ └─┘ └─┘
par ───────┘ └─┘ └─┘
pid ───────┘ └─┘ └┘┴
st ───────────────────────────────────┘└──┘└
253 { intros a b h c ca h₂,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ───────────────────────┘└─
254 cases c with c, {cases h₂},
id ┴ └┘
src └────┘ └─────┘ └────┘
typ └────┘┴└─────┘ └────┘└┘
doc └────┘ └─────┘ └────┘
txt └────┘ └─────┘ └────┘
par └────┘ └─────┘ └────┘
pid ┴ └─────┘ ┴
st ─────────────────┘└─────────┘└┘└
255 cases b with b; cases h₂,
id ┴ └┘
src └────┘ └─────┘ └────┘
typ └────┘┴└─────┘ └────┘└┘
doc └────┘ └─────┘ └────┘
txt └────┘ └─────┘ └────┘
par └────┘ └─────┘ └────┘
pid ┴ └─────┘ ┴
st ───────────────────────────┘└─
256 cases a with a, {cases le_antisymm h le_top },
id ┴ └─────────┘ ┴ └────┘
src └────┘ └─────┘ └────┘└─────────┘┴ ┴└────┘┴
typ └────┘┴└─────┘ └────┘└─────────┘┴┴┴└────┘┴
doc └────┘ └─────┘ └────┘ ┴ ┴ ┴
txt └────┘ └─────┘ └────┘ ┴ ┴ ┴
par └────┘ └─────┘ └────┘ ┴ ┴ ┴
pid ┴ └─────┘ ┴ ┴ ┴ ┴
st ─────────────────┘└────────────────────────────┘└┘└
257 simp at h,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└──┘
st ────────────┘└─
258 exact ⟨_, rfl, add_le_add_left' h⟩, }
id └─┘ └──────────────┘ ┴
src └────┘ └─┘└─┘└┘└──────────────┘┴ ┴
typ └────┘ └─┘└─┘└┘└──────────────┘┴┴┴
doc └────┘ └─┘ └┘ ┴ ┴
txt └────┘ └─┘ └┘ ┴ ┴
par └────┘ └─┘ └┘ ┴ ┴
pid ┴ └─┘ └┘ ┴ ┴
st ─────────────────────────────────────┘└───
259 end
st ──┘
260
261 @[simp] lemma zero_lt_top [ordered_comm_monoid α] : (0 : with_top α) < ⊤ :=
id └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴
src └─────────────────┘ └──────┘ ┴ ┴
typ └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴
doc └──┘ └─────────────────┘
262 coe_lt_top 0
id └────────┘
src └────────┘
typ └────────┘
263
264 @[simp] lemma zero_lt_coe [ordered_comm_monoid α] (a : α) : (0 : with_top α) < a ↔ 0 < a :=
id └─────────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ └──────┘ ┴ ┴ ┴
typ └─────────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────────────┘
265 coe_lt_coe
id └────────┘
src └────────┘
typ └────────┘
266
267 @[simp] lemma add_top [ordered_comm_monoid α] : ∀{a : with_top α}, a + ⊤ = ⊤
id └─────────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ └──────┘ ┴ ┴ ┴ ┴
typ └─────────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────────────┘
268 | none := rfl
id └──┘ └─┘
src └──┘ └─┘
typ └──┘ └─┘
269 | (some a) := rfl
id └──┘ └─┘
src └──┘ └─┘
typ └──┘ └─┘
270
271 @[simp] lemma top_add [ordered_comm_monoid α] {a : with_top α} : ⊤ + a = ⊤ := rfl
id └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────────────────┘ └──────┘ ┴ ┴ ┴ ┴ └─┘
typ └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └─────────────────┘
272
273 lemma add_eq_top [ordered_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
id └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────────┘
274 by cases a; cases b; simp [none_eq_top, some_eq_coe, coe_add.symm]
id ┴ ┴ └─────────┘ └─────────┘
src └────┘ └────┘ └────┘└─────────┘└┘└─────────┘└┘ └─
typ └────┘┴ └────┘┴ └────┘└─────────┘└┘└─────────┘└┘└──────────┘└─
doc └────┘ └────┘ └────┘ └┘ └┘ └─
txt └────┘ └────┘ └────┘ └┘ └┘ └─
par └────┘ └────┘ └────┘ └┘ └┘ └─
pid ┴ ┴ ┴┴ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────
275
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
276 lemma add_lt_top [ordered_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
id └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────────┘
277 begin
st └─────
278 apply not_iff_not.1,
id └─────────┘
src └────┘└─────────┘└┘
typ └────┘└─────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ────────────────────┘└─
279 simp [lt_top_iff_ne_top, add_eq_top],
id └───────────────┘ └────────┘
src └────┘└───────────────┘└┘└────────┘┴
typ └────┘└───────────────┘└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ─────────────────────────────────────┘└─
280 finish,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
281 apply classical.dec _,
id └───────────┘
src └────┘└───────────┘└┘
typ └────┘└───────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ──────────────────────┘└─
282 apply classical.dec _,
id └───────────┘
src └────┘└───────────┘└┘
typ └────┘└───────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ──────────────────────┘└─
283 end
st ──┘
284
285 instance [canonically_ordered_monoid α] : canonically_ordered_monoid (with_top α) :=
id └────────────────────────┘ ┴ └────────────────────────┘ └──────┘ ┴
src └────────────────────────┘ └────────────────────────┘ └──────┘
typ └────────────────────────┘ ┴ └────────────────────────┘ └──────┘ ┴
doc └────────────────────────┘ └────────────────────────┘
286 { le_iff_exists_add := assume a b,
id ┴ ┴
typ ┴ ┴
287 match a, b with
id ┴ ┴
typ ┴ ┴
288 | a, none := show a ≤ ⊤ ↔ ∃c, ⊤ = a + c, by simp; refine ⟨⊤, _⟩; cases a; refl
id ┴ └──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴└──┘ └────┘ └────
typ ┴ └──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴└──┘ └────┘┴ └────
doc └──┘ └─────┘ └──┘ └────┘ └────
txt └──┘ └─────┘ └──┘ └────┘ └────
par └──┘ └─────┘ └──┘ └────┘ └────
pid ┴ └──┘ ┴ └
st └───────────────────────────────────
289 | (some a), (some b) := show (a:with_top α) ≤ ↑b ↔ ∃c:with_top α, ↑b = ↑a + c,
id ┴ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src ─┘ └──┘ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
typ ─┘ ┴ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
290 begin
st └─────
291 simp [canonically_ordered_monoid.le_iff_exists_add, -add_comm],
id └──────────────────────────────────────────┘
src └────┘└──────────────────────────────────────────┘└──────────┘
typ └────┘└──────────────────────────────────────────┘└──────────┘
doc └────┘ └──────────┘
txt └────┘ └──────────┘
par └────┘ └──────────┘
pid ┴┴ └──────────┘
st ───────────────────────────────────────────────────────────────────┘└─
292 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
293 { rintro ⟨c, rfl⟩, refine ⟨c, _⟩, simp [coe_add] },
id ┴ └─────┘
src └─────────────┘ └─────┘ └──┘ └────┘└─────┘└┘
typ └─────────────┘ └─────┘ ┴└──┘ └────┘└─────┘└┘
doc └─────────────┘ └─────┘ └──┘ └────┘ └┘
txt └─────────────┘ └─────┘ └──┘ └────┘ └┘
par └─────────────┘ └─────┘ └──┘ └────┘ └┘
pid └───────┘ ┴ └──┘ ┴┴ ┴┴
st ───────┘└─────────────┘└─────────────┘└───────────────┘└┘└
294 { exact assume h, match b, h with _, ⟨some c, rfl⟩ := ⟨_, rfl⟩ end }
id ┴ └──┘ └─┘
src └────┘ └──┘ ┴ └┘ └───────┘ └──┘┴ └┘ └───┘ └─┘└─┘└────┘
typ └────┘ └──┘ ┴┴└┘ └───────┘ └──┘┴ └┘ └───┘ └─┘└─┘└────┘
doc └────┘ └──┘ ┴ └┘ └───────┘ ┴ └┘ └───┘ └─┘ └────┘
txt └────┘ └──┘ ┴ └┘ └───────┘ ┴ └┘ └───┘ └─┘ └────┘
par └────┘ └──┘ ┴ └┘ └───────┘ ┴ └┘ └───┘ └─┘ └────┘
pid ┴ └──┘ ┴ └┘ └───────┘ ┴ └┘ └───┘ └─┘ └───┘┴
st ────────────────────────────────────────────────────────────────────────┘└─
295 end
st ──────┘
296 | none, some b := show (⊤ : with_top α) ≤ b ↔ ∃c:with_top α, ↑b = ⊤ + c, by simp
id └──┘ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └────
typ └──┘ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
297 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
298 .. with_top.order_bot,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
299 .. with_top.ordered_comm_monoid }
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
300
301 end with_top
302
303 namespace with_bot
304 open lattice
305
306 instance [add_semigroup α] : add_semigroup (with_bot α) := with_top.add_semigroup
id └───────────┘ ┴ └───────────┘ └──────┘ ┴ └────────────────────┘
src └───────────┘ └───────────┘ └──────┘ └────────────────────┘
typ └───────────┘ ┴ └───────────┘ └──────┘ ┴ └────────────────────┘
307 instance [add_comm_semigroup α] : add_comm_semigroup (with_bot α) := with_top.add_comm_semigroup
id └────────────────┘ ┴ └────────────────┘ └──────┘ ┴ └─────────────────────────┘
src └────────────────┘ └────────────────┘ └──────┘ └─────────────────────────┘
typ └────────────────┘ ┴ └────────────────┘ └──────┘ ┴ └─────────────────────────┘
308 instance [add_monoid α] : add_monoid (with_bot α) := with_top.add_monoid
id └────────┘ ┴ └────────┘ └──────┘ ┴ └─────────────────┘
src └────────┘ └────────┘ └──────┘ └─────────────────┘
typ └────────┘ ┴ └────────┘ └──────┘ ┴ └─────────────────┘
309 instance [add_comm_monoid α] : add_comm_monoid (with_bot α) := with_top.add_comm_monoid
id └─────────────┘ ┴ └─────────────┘ └──────┘ ┴ └──────────────────────┘
src └─────────────┘ └─────────────┘ └──────┘ └──────────────────────┘
typ └─────────────┘ ┴ └─────────────┘ └──────┘ ┴ └──────────────────────┘
310
311 instance [ordered_comm_monoid α] : ordered_comm_monoid (with_bot α) :=
id └─────────────────┘ ┴ └─────────────────┘ └──────┘ ┴
src └─────────────────┘ └─────────────────┘ └──────┘
typ └─────────────────┘ ┴ └─────────────────┘ └──────┘ ┴
doc └─────────────────┘ └─────────────────┘
312 begin
st └─────
313 suffices, refine {
src └──────┘ └─────┘ └
typ └──────┘ └─────┘ └
doc └──────┘ └─────┘ └
txt └──────┘ └─────┘ └
par └──────┘ └─────┘ └
pid └──────┘ ┴ └
st ─────────┘└──────────
314 add_le_add_left := this,
id └──┘
src ──────────────────────┘ └─
typ ──────────────────────┘└──┘└─
doc ──────────────────────┘ └─
txt ──────────────────────┘ └─
par ──────────────────────┘ └─
pid ──────────────────────┘ └─
st ─────────────────────────────
315 ..with_bot.partial_order,
id └────────────────────┘
src ─────┘└────────────────────┘└─
typ ─────┘└────────────────────┘└─
doc ─────┘ └─
txt ─────┘ └─
par ─────┘ └─
pid ─────┘ └─
st ──────────────────────────────
316 ..with_bot.add_comm_monoid, ..},
id └──────────────────────┘
src ─────┘└──────────────────────┘└───┘
typ ─────┘└──────────────────────┘└───┘
doc ─────┘ └───┘
txt ─────┘ └───┘
par ─────┘ └───┘
pid ─────┘ └───┘
st ──────────────────────────────────┘└─
317 { intros a b c h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
318 have h' := h,
id ┴
src └─────────┘
typ └─────────┘┴
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────┘┴└─┘
st ───────────────┘└─
319 rw lt_iff_le_not_le at h' ⊢,
id └──────────────┘
src └─┘└──────────────┘└──────┘
typ └─┘└──────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ──────────────────────────────┘└─
320 refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
id └┘ └──┘
src └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
typ └─────┘ └────────┘ └───┘└┘└─┘ ┴└──┘└───┘ └─┘
doc └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
txt └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
par └─────┘ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
pid ┴ └────────┘ └───┘ └─┘ ┴ └───┘ └─┘
st ─────────────────────────────────────────────────┘└─
321 cases h₂, cases a with a,
id └┘ ┴
src └────┘ └────┘ └─────┘
typ └────┘└┘ └────┘┴└─────┘
doc └────┘ └────┘ └─────┘
txt └────┘ └────┘ └─────┘
par └────┘ └────┘ └─────┘
pid ┴ ┴ └─────┘
st ───────────┘└──────────────┘└─
322 { exact (not_le_of_lt h).elim bot_le },
id └──────────┘ ┴ └────┘
src └────┘ └──────────┘┴ └─────┘└────┘┴
typ └────┘ └──────────┘┴┴└─────┘└────┘┴
doc └────┘ ┴ └─────┘ ┴
txt └────┘ ┴ └─────┘ ┴
par └────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ─────┘└─────────────────────────────────┘└┘└
323 cases c with c,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
324 { exact (not_le_of_lt h).elim bot_le },
id └──────────┘ ┴ └────┘
src └────┘ └──────────┘┴ └─────┘└────┘┴
typ └────┘ └──────────┘┴┴└─────┘└────┘┴
doc └────┘ ┴ └─────┘ ┴
txt └────┘ ┴ └─────┘ ┴
par └────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ─────┘└─────────────────────────────────┘└┘└
325 { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left' $
id └─┘ └──────┘ └────────────────────┘
src └────┘ └─┘└─┘└┘└──────┘┴ └────────────────────┘┴ └
typ └────┘ └─┘└─┘└┘└──────┘┴ └────────────────────┘┴ └
doc └────┘ └─┘ └┘ ┴ ┴ └
txt └────┘ └─┘ └┘ ┴ ┴ └
par └────┘ └─┘ └┘ ┴ ┴ └
pid ┴ └─┘ └┘ ┴ ┴ └
st ────────────────────────────────────────────────────────
326 with_bot.some_lt_some.1 h)⟩ } },
id └───────────────────┘ ┴
src ───────┘└───────────────────┘└─┘ └─┘
typ ───────┘└───────────────────┘└─┘┴└─┘
doc ───────┘ └─┘ └─┘
txt ───────┘ └─┘ └─┘
par ───────┘ └─┘ └─┘
pid ───────┘ └─┘ └┘┴
st ───────────────────────────────────┘└──┘└
327 { intros a b h c ca h₂,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ───────────────────────┘└─
328 cases c with c, {cases h₂},
id ┴ └┘
src └────┘ └─────┘ └────┘
typ └────┘┴└─────┘ └────┘└┘
doc └────┘ └─────┘ └────┘
txt └────┘ └─────┘ └────┘
par └────┘ └─────┘ └────┘
pid ┴ └─────┘ ┴
st ─────────────────┘└─────────┘└┘└
329 cases a with a; cases h₂,
id ┴ └┘
src └────┘ └─────┘ └────┘
typ └────┘┴└─────┘ └────┘└┘
doc └────┘ └─────┘ └────┘
txt └────┘ └─────┘ └────┘
par └────┘ └─────┘ └────┘
pid ┴ └─────┘ ┴
st ───────────────────────────┘└─
330 cases b with b, {cases le_antisymm h bot_le},
id ┴ └─────────┘ ┴ └────┘
src └────┘ └─────┘ └────┘└─────────┘┴ ┴└────┘
typ └────┘┴└─────┘ └────┘└─────────┘┴┴┴└────┘
doc └────┘ └─────┘ └────┘ ┴ ┴
txt └────┘ └─────┘ └────┘ ┴ ┴
par └────┘ └─────┘ └────┘ ┴ ┴
pid ┴ └─────┘ ┴ ┴ ┴
st ─────────────────┘└───────────────────────────┘└┘└
331 simp at h,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└──┘
st ────────────┘└─
332 exact ⟨_, rfl, add_le_add_left' h⟩, }
id └─┘ └──────────────┘ ┴
src └────┘ └─┘└─┘└┘└──────────────┘┴ ┴
typ └────┘ └─┘└─┘└┘└──────────────┘┴┴┴
doc └────┘ └─┘ └┘ ┴ ┴
txt └────┘ └─┘ └┘ ┴ ┴
par └────┘ └─┘ └┘ ┴ ┴
pid ┴ └─┘ └┘ ┴ ┴
st ─────────────────────────────────────┘└───
333 end
st ──┘
334
335 @[simp] lemma coe_zero [add_monoid α] : ((0 : α) : with_bot α) = 0 := rfl
id └────────┘ ┴ ┴ └──────┘ ┴ ┴ └─┘
src └────────┘ └──────┘ ┴ └─┘
typ └────────┘ ┴ ┴ └──────┘ ┴ ┴ └─┘
doc └──┘
336
337 @[simp] lemma coe_add [add_semigroup α] (a b : α) : ((a + b : α) : with_bot α) = a + b := rfl
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └───────────┘ ┴ └──────┘ ┴ ┴ └─┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
338
339 @[simp] lemma bot_add [ordered_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl
id └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────────────────┘ └──────┘ ┴ ┴ ┴ ┴ └─┘
typ └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └─────────────────┘
340
341 @[simp] lemma add_bot [ordered_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl
id └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ └──────┘ ┴ ┴ ┴ ┴ └────┘ └────
typ └─────────────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ └────
doc └──┘ └─────────────────┘ └────┘ └────
txt └────┘ └────
par └────┘ └────
pid ┴ └
st └──────────────
342
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
343 instance has_one [has_one α] : has_one (with_bot α) := ⟨(1 : α)⟩
id └─────┘ ┴ └─────┘ └──────┘ ┴ ┴
src └─────┘ └─────┘ └──────┘
typ └─────┘ ┴ └─────┘ └──────┘ ┴ ┴
344
345 @[simp] lemma coe_one [has_one α] : ((1 : α) : with_bot α) = 1 := rfl
id └─────┘ ┴ ┴ └──────┘ ┴ ┴ └─┘
src └─────┘ └──────┘ ┴ └─┘
typ └─────┘ ┴ ┴ └──────┘ ┴ ┴ └─┘
doc └──┘
346
347 end with_bot
348
349 section canonically_ordered_monoid
350 variables [canonically_ordered_monoid α] {a b c d : α}
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
doc └────────────────────────┘
351
352 lemma le_iff_exists_add : a ≤ b ↔ ∃c, b = a + c :=
id ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
353 canonically_ordered_monoid.le_iff_exists_add a b
id └──────────────────────────────────────────┘ ┴ ┴
src └──────────────────────────────────────────┘
typ └──────────────────────────────────────────┘ ┴ ┴
354
355 @[simp] lemma zero_le (a : α) : 0 ≤ a := le_iff_exists_add.mpr ⟨a, by simp⟩
id ┴ ┴ ┴ └───────────────┘└──┘ ┴
src ┴ └───────────────┘└──┘ └──┘
typ ┴ ┴ ┴ └───────────────┘└──┘ ┴ └──┘
doc └──┘ └──┘
txt └──┘
par └──┘
st └───┘
356
357 lemma bot_eq_zero : (⊥ : α) = 0 :=
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
358 le_antisymm lattice.bot_le (zero_le ⊥)
id └─────────┘ └────────────┘ └─────┘ ┴
src └─────────┘ └────────────┘ └─────┘ ┴
typ └─────────┘ └────────────┘ └─────┘ ┴
359
360 @[simp] lemma add_eq_zero_iff : a + b = 0 ↔ a = 0 ∧ b = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
361 add_eq_zero_iff' (zero_le _) (zero_le _)
id └──────────────┘ └─────┘ └─────┘
src └──────────────┘ └─────┘ └─────┘
typ └──────────────┘ └─────┘ └─────┘
362
363 @[simp] lemma le_zero_iff_eq : a ≤ 0 ↔ a = 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
364 iff.intro
id └───────┘
src └───────┘
typ └───────┘
365 (assume h, le_antisymm h (zero_le a))
id ┴ └─────────┘ ┴ └─────┘ ┴
src └─────────┘ └─────┘
typ ┴ └─────────┘ ┴ └─────┘ ┴
366 (assume h, h ▸ le_refl a)
id ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴
367
368 protected lemma zero_lt_iff_ne_zero : 0 < a ↔ a ≠ 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
369 iff.intro ne_of_gt $ assume hne, lt_of_le_of_ne (zero_le _) hne.symm
id └───────┘ └──────┘ └─┘ └────────────┘ └─────┘ └─┘└───┘
src └───────┘ └──────┘ └────────────┘ └─────┘ └───┘
typ └───────┘ └──────┘ └─┘ └────────────┘ └─────┘ └─┘└───┘
370
371 lemma le_add_left (h : a ≤ c) : a ≤ b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
372 calc a = 0 + a : by simp
id ┴ ┴ ┴
src ┴ └────
typ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
373 ... ≤ b + c : add_le_add' (zero_le _) h
id ┴ ┴ ┴ └─────────┘ └─────┘ ┴
src ─┘ ┴ └─────────┘ └─────┘
typ ─┘ ┴ ┴ ┴ └─────────┘ └─────┘ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
374
375 lemma le_add_right (h : a ≤ b) : a ≤ b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
376 calc a = a + 0 : by simp
id ┴ ┴ ┴
src ┴ └────
typ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
377 ... ≤ b + c : add_le_add' h (zero_le _)
id ┴ ┴ ┴ └─────────┘ ┴ └─────┘
src ─┘ ┴ └─────────┘ └─────┘
typ ─┘ ┴ ┴ ┴ └─────────┘ ┴ └─────┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
378
379 instance with_zero.canonically_ordered_monoid :
380 canonically_ordered_monoid (with_zero α) :=
id └────────────────────────┘ └───────┘ ┴
src └────────────────────────┘ └───────┘
typ └────────────────────────┘ └───────┘ ┴
doc └────────────────────────┘
381 { le_iff_exists_add := λ a b, begin
id ┴ ┴
typ ┴ ┴
st └─────
382 cases a with a,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
383 { exact iff_of_true lattice.bot_le ⟨b, (zero_add b).symm⟩ },
id └─────────┘ └────────────┘ └──────┘ ┴
src └────┘└─────────┘┴└────────────┘┴ └┘ └──────┘┴ └──────┘
typ └────┘└─────────┘┴└────────────┘┴ └┘ └──────┘┴┴└──────┘
doc └────┘ ┴ ┴ └┘ ┴ └──────┘
txt └────┘ ┴ ┴ └┘ ┴ └──────┘
par └────┘ ┴ ┴ └┘ ┴ └──────┘
pid ┴ ┴ ┴ └┘ ┴ └─────┘┴
st ─────┘└──────────────────────────────────────────────────────┘└┘└
384 cases b with b,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
385 { exact iff_of_false
id └──────────┘
src └────┘└──────────┘└
typ └────┘└──────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────┘└──────────────────
386 (mt (le_antisymm lattice.bot_le) (by simp))
id └┘ └─────────┘ └────────────┘
src ───────┘ └┘┴ └─────────┘┴└────────────┘└┘ ┴└──┘└──
typ ───────┘ └┘┴ └─────────┘┴└────────────┘└┘ ┴└──┘└──
doc ───────┘ ┴ ┴ └┘ ┴└──┘└──
txt ───────┘ ┴ ┴ └┘ ┴└──┘└──
par ───────┘ ┴ ┴ └┘ ┴└──┘└──
pid ───────┘ ┴ ┴ └┘ └───────
st ───────────────────────────────────────────┘└───┘└──
387 (λ ⟨c, h⟩, by cases c; cases h) },
id ┴ ┴
src ───────┘ └┘ └┘ └─┘ ┴└────┘ └┘└────┘ └┘
typ ───────┘ └┘ └┘ └─┘ ┴└────┘┴└┘└────┘┴└┘
doc ───────┘ └┘ └┘ └─┘ ┴└────┘ └┘└────┘ └┘
txt ───────┘ └┘ └┘ └─┘ ┴└────┘ └┘└────┘ └┘
par ───────┘ └┘ └┘ └─┘ ┴└────┘ └┘└────┘ └┘
pid ───────┘ └┘ └┘ └─┘ └─────┘ └──────┘ ┴┴
st ────────────────────┘└───────────────┘└┘└┘└
388 { simp [le_iff_exists_add, -add_comm],
id └───────────────┘
src └────┘└───────────────┘└──────────┘
typ └────┘└───────────────┘└──────────┘
doc └────┘ └──────────┘
txt └────┘ └──────────┘
par └────┘ └──────────┘
pid ┴┴ └──────────┘
st ────────────────────────────────────────┘└─
389 split; intro h; rcases h with ⟨c, h⟩,
id ┴
src └───┘ └─────┘ └─────┘ └──────────┘
typ └───┘ └─────┘ └─────┘┴└──────────┘
doc └───┘ └─────┘ └─────┘ └──────────┘
txt └───┘ └─────┘ └─────┘ └──────────┘
par └───┘ └─────┘ └─────┘ └──────────┘
pid └┘ ┴ └──────────┘
st ─────────────────────────────────────────┘└─
390 { exact ⟨some c, congr_arg some h⟩ },
id ┴ └───────┘ └──┘ ┴
src └────┘ ┴ └┘└───────┘┴└──┘┴ └┘
typ └────┘ ┴┴└┘└───────┘┴└──┘┴┴└┘
doc └────┘ ┴ └┘ ┴ ┴ └┘
txt └────┘ ┴ └┘ ┴ ┴ └┘
par └────┘ ┴ └┘ ┴ ┴ └┘
pid ┴ ┴ └┘ ┴ ┴ ┴┴
st ───────┘└───────────────────────────────┘└┘└
391 { cases c; cases h,
id ┴ ┴
src └────┘ └────┘
typ └────┘┴ └────┘┴
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ───────────────────────┘└─
392 { exact ⟨_, (add_zero _).symm⟩ },
id └──────┘
src └────┘ └─┘ └──────┘└────────┘
typ └────┘ └─┘ └──────┘└────────┘
doc └────┘ └─┘ └────────┘
txt └────┘ └─┘ └────────┘
par └────┘ └─┘ └────────┘
pid ┴ └─┘ └───────┘┴
st ─────────┘└───────────────────────────┘└┘└
393 { exact ⟨_, rfl⟩ } } }
id └─┘
src └────┘ └─┘└─┘└┘
typ └────┘ └─┘└─┘└┘
doc └────┘ └─┘ └┘
txt └────┘ └─┘ └┘
par └────┘ └─┘ └┘
pid ┴ └─┘ ┴┴
st ────────────────────────┘└─────
394 end,
st ────┘
395 bot := 0,
396 bot_le := assume a a' h, option.no_confusion h,
id ┴ └┘ ┴ └─────────────────┘ ┴
src └─────────────────┘
typ ┴ └┘ ┴ └─────────────────┘ ┴
397 .. with_zero.ordered_comm_monoid zero_le }
id └───────────────────────────┘ └─────┘
src └───────────────────────────┘ └─────┘
typ └───────────────────────────┘ └─────┘
398
399 end canonically_ordered_monoid
400
401 @[priority 100] -- see Note [lower instance priority]
402 instance ordered_cancel_comm_monoid.to_ordered_comm_monoid
403 [H : ordered_cancel_comm_monoid α] : ordered_comm_monoid α :=
id └────────────────────────┘ ┴ └─────────────────┘ ┴
src └────────────────────────┘ └─────────────────┘
typ └────────────────────────┘ ┴ └─────────────────┘ ┴
doc └─────────────────┘
404 { lt_of_add_lt_add_left := @lt_of_add_lt_add_left _ _, ..H }
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
405
406 section ordered_cancel_comm_monoid
407 variables [ordered_cancel_comm_monoid α] {a b c x y : α}
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
408
409 @[simp] lemma add_le_add_iff_left (a : α) {b c : α} : a + b ≤ a + c ↔ b ≤ c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
410 ⟨le_of_add_le_add_left, λ h, add_le_add_left h _⟩
id └───────────────────┘ ┴ └─────────────┘ ┴
src └───────────────────┘ └─────────────┘
typ └───────────────────┘ ┴ └─────────────┘ ┴
411
412 @[simp] lemma add_le_add_iff_right (c : α) : a + c ≤ b + c ↔ a ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
413 add_comm c a ▸ add_comm c b ▸ add_le_add_iff_left c
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─────────────────┘ ┴
src └──────┘ ┴ └──────┘ ┴ └─────────────────┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─────────────────┘ ┴
414
415 @[simp] lemma add_lt_add_iff_left (a : α) {b c : α} : a + b < a + c ↔ b < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
416 ⟨lt_of_add_lt_add_left, λ h, add_lt_add_left h _⟩
id └───────────────────┘ ┴ └─────────────┘ ┴
src └───────────────────┘ └─────────────┘
typ └───────────────────┘ ┴ └─────────────┘ ┴
417
418 @[simp] lemma add_lt_add_iff_right (c : α) : a + c < b + c ↔ a < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
419 add_comm c a ▸ add_comm c b ▸ add_lt_add_iff_left c
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─────────────────┘ ┴
src └──────┘ ┴ └──────┘ ┴ └─────────────────┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─────────────────┘ ┴
420
421 @[simp] lemma le_add_iff_nonneg_right (a : α) {b : α} : a ≤ a + b ↔ 0 ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
422 have a + 0 ≤ a + b ↔ 0 ≤ b, from add_le_add_iff_left a,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
423 by rwa add_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
424
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
425 @[simp] lemma le_add_iff_nonneg_left (a : α) {b : α} : a ≤ b + a ↔ 0 ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
426 by rw [add_comm, le_add_iff_nonneg_right]
id └──────┘ └─────────────────────┘
src └──┘└──────┘└┘└─────────────────────┘└─
typ └──┘└──────┘└┘└─────────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────┘└───────────────────────┘┴└
427
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
428 @[simp] lemma lt_add_iff_pos_right (a : α) {b : α} : a < a + b ↔ 0 < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
429 have a + 0 < a + b ↔ 0 < b, from add_lt_add_iff_left a,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
430 by rwa add_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
431
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
432 @[simp] lemma lt_add_iff_pos_left (a : α) {b : α} : a < b + a ↔ 0 < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
433 by rw [add_comm, lt_add_iff_pos_right]
id └──────┘ └──────────────────┘
src └──┘└──────┘└┘└──────────────────┘└─
typ └──┘└──────┘└┘└──────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────┘└────────────────────┘┴└
434
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
435 @[simp] lemma add_le_iff_nonpos_left : x + y ≤ y ↔ x ≤ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
436 by { convert add_le_add_iff_right y, rw [zero_add] }
id └──────────────────┘ ┴ └──────┘
src └──────┘└──────────────────┘┴ └──┘└──────┘└┘
typ └──────┘└──────────────────┘┴┴ └──┘└──────┘└┘
doc └──────┘ ┴ └──┘ └┘
txt └──────┘ ┴ └──┘ └┘
par └──────┘ ┴ └──┘ └┘
pid ┴ ┴ └┘ ┴┴
st └───────────────────────────────┘└────────────┘┴┴└┘
437
438 @[simp] lemma add_le_iff_nonpos_right : x + y ≤ x ↔ y ≤ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
439 by { convert add_le_add_iff_left x, rw [add_zero] }
id └─────────────────┘ ┴ └──────┘
src └──────┘└─────────────────┘┴ └──┘└──────┘└┘
typ └──────┘└─────────────────┘┴┴ └──┘└──────┘└┘
doc └──────┘ ┴ └──┘ └┘
txt └──────┘ ┴ └──┘ └┘
par └──────┘ ┴ └──┘ └┘
pid ┴ ┴ └┘ ┴┴
st └──────────────────────────────┘└────────────┘┴┴└┘
440
441 @[simp] lemma add_lt_iff_neg_right : x + y < y ↔ x < 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
442 by { convert add_lt_add_iff_right y, rw [zero_add] }
id └──────────────────┘ ┴ └──────┘
src └──────┘└──────────────────┘┴ └──┘└──────┘└┘
typ └──────┘└──────────────────┘┴┴ └──┘└──────┘└┘
doc └──────┘ ┴ └──┘ └┘
txt └──────┘ ┴ └──┘ └┘
par └──────┘ ┴ └──┘ └┘
pid ┴ ┴ └┘ ┴┴
st └───────────────────────────────┘└────────────┘┴┴└┘
443
444 @[simp] lemma add_lt_iff_neg_left : x + y < x ↔ y < 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
445 by { convert add_lt_add_iff_left x, rw [add_zero] }
id └─────────────────┘ ┴ └──────┘
src └──────┘└─────────────────┘┴ └──┘└──────┘└┘
typ └──────┘└─────────────────┘┴┴ └──┘└──────┘└┘
doc └──────┘ ┴ └──┘ └┘
txt └──────┘ ┴ └──┘ └┘
par └──────┘ ┴ └──┘ └┘
pid ┴ ┴ └┘ ┴┴
st └──────────────────────────────┘└────────────┘┴┴└┘
446
447 lemma add_eq_zero_iff_eq_zero_of_nonneg
448 (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
449 ⟨λ hab : a + b = 0,
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
450 by split; apply le_antisymm; try {assumption};
id └─────────┘
src └───┘ └────┘└─────────┘ └───┘└────────┘┴
typ └───┘ └────┘└─────────┘ └───┘└────────┘┴
doc └───┘ └────┘ └───┘└────────┘┴
txt └───┘ └────┘ └───┘└────────┘┴
par └───┘ └────┘ └───┘└────────┘┴
pid ┴ └───────────┘
st └──────────────────────────────┘└────────┘└┘└
451 rw ← hab; simp [ha, hb],
id └─┘ └┘ └┘
src └───┘ └────┘ └┘ ┴
typ └───┘└─┘ └────┘└┘└┘└┘┴
doc └───┘ └────┘ └┘ ┴
txt └───┘ └────┘ └┘ ┴
par └───┘ └────┘ └┘ ┴
pid └─┘ ┴┴ └┘ ┴
st ─────────────────────────┘
452 λ ⟨ha', hb'⟩, by rw [ha', hb', add_zero]⟩
id ┴ └─┘ └─┘ └──────┘
src └──┘ └┘ └┘└──────┘┴
typ ┴ └──┘└─┘└┘└─┘└┘└──────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └──────┘└───┘└────────┘┴
453
454 lemma with_top.add_lt_add_iff_left :
455 ∀{a b c : with_top α}, a < ⊤ → (a + c < a + b ↔ c < b)
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
456 | none := assume b c h, (lt_irrefl ⊤ h).elim
id └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └──┘
src └──┘ └───────┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └──┘
457 | (some a) :=
id └──┘
src └──┘
typ └──┘
458 begin
st └─────
459 assume b c h,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───────────────┘└─
460 cases b; cases c;
id ┴ ┴
src └────┘ └────┘
typ └────┘┴ └────┘┴
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ──────────────────────
461 simp [with_top.none_eq_top, with_top.some_eq_coe, with_top.coe_lt_top, with_top.coe_lt_coe],
id └──────────────────┘ └──────────────────┘ └─────────────────┘ └─────────────────┘
src └────┘└──────────────────┘└┘└──────────────────┘└┘└─────────────────┘└┘└─────────────────┘┴
typ └────┘└──────────────────┘└┘└──────────────────┘└┘└─────────────────┘└┘└─────────────────┘┴
doc └────┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
462 { rw [← with_top.coe_add], exact with_top.coe_lt_top _ },
id └──────────────┘ └─────────────────┘
src └────┘└──────────────┘┴ └────┘└─────────────────┘└─┘
typ └────┘└──────────────┘┴ └────┘└─────────────────┘└─┘
doc └────┘ ┴ └────┘ └─┘
txt └────┘ ┴ └────┘ └─┘
par └────┘ ┴ └────┘ └─┘
pid └──┘ ┴ ┴ └┘┴
st ─────┘└────────────────────┘┴└────────────────────────────┘└┘└
463 { rw [← with_top.coe_add, ← with_top.coe_add, with_top.coe_lt_coe],
id └──────────────┘ └──────────────┘ └─────────────────┘
src └────┘└──────────────┘└──┘└──────────────┘└┘└─────────────────┘┴
typ └────┘└──────────────┘└──┘└──────────────┘└┘└─────────────────┘┴
doc └────┘ └──┘ └┘ ┴
txt └────┘ └──┘ └┘ ┴
par └────┘ └──┘ └┘ ┴
pid └──┘ └──┘ └┘ ┴
st ───────────────────────────┘└──────────────────┘└───────────────────┘┴└─
464 exact add_lt_add_iff_left _ }
id └─────────────────┘
src └────┘└─────────────────┘└─┘
typ └────┘└─────────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────────────────────────┘└─
465 end
st ────┘
466
467 lemma with_top.add_lt_add_iff_right
468 {a b c : with_top α} : a < ⊤ → (c + a < b + a ↔ c < b) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
469 by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c
id └──────┘ └──────────────────────────┘ ┴ ┴ ┴
src └─────┘└──────┘└──────┘ └──────────────────────────┘└───┘ ┴ ┴ └
typ └─────┘└──────┘└──────┘ └──────────────────────────┘└───┘┴┴┴┴┴└
doc └─────┘ └──────┘ └───┘ ┴ ┴ └
txt └─────┘ └──────┘ └───┘ ┴ ┴ └
par └─────┘ └──────┘ └───┘ ┴ ┴ └
pid ┴┴ ┴┴└────┘ └───┘ ┴ ┴ └
st └───────────────────────────────────────────────────────────────
470
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
471 end ordered_cancel_comm_monoid
472
473 section ordered_comm_group
474
475 /--
476 The `add_lt_add_left` field of `ordered_comm_group` is redundant, but it is in core so
477 we can't remove it for now. This alternative constructor is the best we can do.
478 -/
479 def ordered_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α]
id └────────────┘ ┴ └───────────┘ ┴
src └────────────┘ └───────────┘
typ └────────────┘ ┴ └───────────┘ ┴
480 (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
481 ordered_comm_group α :=
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
482 { add_le_add_left := add_le_add_left,
id └─────────────┘
src └─────────────┘
typ └─────────────┘
483 add_lt_add_left := λ a b h c,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
484 begin
st └─────
485 rw lt_iff_le_not_le at h,
id └──────────────┘
src └─┘└──────────────┘└───┘
typ └─┘└──────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────────────────┘└─
486 rw lt_iff_le_not_le,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘└─
487 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
488 { apply add_le_add_left _ _ h.1 },
id └─────────────┘ ┴
src └────┘└─────────────┘└───┘ └─┘
typ └────┘└─────────────┘└───┘┴└─┘
doc └────┘ └───┘ └─┘
txt └────┘ └───┘ └─┘
par └────┘ └───┘ └─┘
pid ┴ └───┘ └─┘
st ─────┘└────────────────────────────┘└┘└
489 { intro w,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────────┘└─
490 replace w : -c + (c + b) ≤ -c + (c + a) := add_le_add_left _ _ w _,
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴
src └──────────┘┴ ┴┴┴ ┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴ └───┘└─────────────┘└───┘ └┘
typ └──────────┘┴ ┴┴┴ ┴ ┴┴└┘┴┴ ┴ ┴ ┴┴ ┴┴└───┘└─────────────┘└───┘┴└┘
doc └──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘ └───┘ └┘
txt └──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘ └───┘ └┘
par └──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘ └───┘ └┘
pid └┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └───┘ └┘
st ───────────────────────────────────────────────────────────────────────┘└─
491 simp only [add_zero, add_comm, add_left_neg, add_left_comm] at w,
id └──────┘ └──────┘ └──────────┘ └───────────┘
src └─────────┘└──────┘└┘└──────┘└┘└──────────┘└┘└───────────┘└────┘
typ └─────────┘└──────┘└┘└──────┘└┘└──────────┘└┘└───────────┘└────┘
doc └─────────┘ └┘ └┘ └┘ └────┘
txt └─────────┘ └┘ └┘ └┘ └────┘
par └─────────┘ └┘ └┘ └┘ └────┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴└──┘
st ─────────────────────────────────────────────────────────────────────┘└─
492 exact h.2 w },
id ┴ ┴
src └────┘ └─┘ ┴
typ └────┘┴└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────┘└──
493 end,
st ────┘
494 ..(by apply_instance : add_comm_group α),
id └────────────┘ ┴
src └─────────────┘ └────────────┘
typ └─────────────┘ └────────────┘ ┴
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
495 ..(by apply_instance : partial_order α) }
id └───────────┘ ┴
src └─────────────┘ └───────────┘
typ └─────────────┘ └───────────┘ ┴
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
496
497 variables [ordered_comm_group α] {a b c : α}
id └────────────────┘
src └────────────────┘
typ └────────────────┘
498
499 lemma neg_neg_iff_pos {α : Type} [_inst_1 : ordered_comm_group α] {a : α} : -a < 0 ↔ 0 < a :=
id └────────────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
500 ⟨ pos_of_neg_neg, neg_neg_of_pos ⟩
id └────────────┘ └────────────┘
src └────────────┘ └────────────┘
typ └────────────┘ └────────────┘
501
502 @[simp] lemma neg_le_neg_iff : -a ≤ -b ↔ b ≤ a :=
id ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘
503 have a + b + -a ≤ a + b + -b ↔ -a ≤ -b, from add_le_add_iff_left _,
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └─────────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └─────────────────┘
504 by simp at this; simp [this]
id └──┘
src └──────────┘ └────┘ └─
typ └──────────┘ └────┘└──┘└─
doc └──────────┘ └────┘ └─
txt └──────────┘ └────┘ └─
par └──────────┘ └────┘ └─
pid ┴└─────┘ ┴┴ ┴└
st └──────────────────────────
505
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
506 lemma neg_le : -a ≤ b ↔ -b ≤ a :=
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
507 have -a ≤ -(-b) ↔ -b ≤ a, from neg_le_neg_iff,
id ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ └────────────┘
508 by rwa neg_neg at this
id └─────┘
src └──┘└─────┘└────────
typ └──┘└─────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────
509
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
510 lemma le_neg : a ≤ -b ↔ b ≤ -a :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴
511 have -(-a) ≤ -b ↔ b ≤ -a, from neg_le_neg_iff,
id ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └────────────┘
512 by rwa neg_neg at this
id └─────┘
src └──┘└─────┘└────────
typ └──┘└─────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────
513
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
514 lemma neg_le_iff_add_nonneg : -a ≤ b ↔ 0 ≤ a + b :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
515 (add_le_add_iff_left a).symm.trans $ by rw add_neg_self
id └─────────────────┘ ┴ └──┘ └───┘ └──────────┘
src └─────────────────┘ └──┘ └───┘ └─┘└──────────┘└
typ └─────────────────┘ ┴ └──┘ └───┘ └─┘└──────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └────────────────
516
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
517 lemma le_neg_iff_add_nonpos : a ≤ -b ↔ a + b ≤ 0 :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
518 (add_le_add_iff_right b).symm.trans $ by rw neg_add_self
id └──────────────────┘ ┴ └──┘ └───┘ └──────────┘
src └──────────────────┘ └──┘ └───┘ └─┘└──────────┘└
typ └──────────────────┘ ┴ └──┘ └───┘ └─┘└──────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └────────────────
519
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
520 @[simp] lemma neg_nonpos : -a ≤ 0 ↔ 0 ≤ a :=
id ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴
doc └──┘
521 have -a ≤ -0 ↔ 0 ≤ a, from neg_le_neg_iff,
id ┴┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
522 by rwa neg_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
523
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
524 @[simp] lemma neg_nonneg : 0 ≤ -a ↔ a ≤ 0 :=
id ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴
doc └──┘
525 have -0 ≤ -a ↔ a ≤ 0, from neg_le_neg_iff,
id ┴ ┴ ┴┴ ┴ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴ ┴ ┴┴ ┴ ┴ ┴ └────────────┘
526 by rwa neg_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
527
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
528 lemma neg_le_self (h : 0 ≤ a) : -a ≤ a :=
id ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴
529 le_trans (neg_nonpos.2 h) h
id └──────┘ └────────┘┴ ┴ ┴
src └──────┘ └────────┘┴
typ └──────┘ └────────┘┴ ┴ ┴
530
531 lemma self_le_neg (h : a ≤ 0) : a ≤ -a :=
id ┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴
532 le_trans h (neg_nonneg.2 h)
id └──────┘ ┴ └────────┘┴ ┴
src └──────┘ └────────┘┴
typ └──────┘ ┴ └────────┘┴ ┴
533
534 @[simp] lemma neg_lt_neg_iff : -a < -b ↔ b < a :=
id ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘
535 have a + b + -a < a + b + -b ↔ -a < -b, from add_lt_add_iff_left _,
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └─────────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └─────────────────┘
536 by simp at this; simp [this]
id └──┘
src └──────────┘ └────┘ └─
typ └──────────┘ └────┘└──┘└─
doc └──────────┘ └────┘ └─
txt └──────────┘ └────┘ └─
par └──────────┘ └────┘ └─
pid ┴└─────┘ ┴┴ ┴└
st └──────────────────────────
537
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
538 lemma neg_lt_zero : -a < 0 ↔ 0 < a :=
id ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴
539 have -a < -0 ↔ 0 < a, from neg_lt_neg_iff,
id ┴┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
540 by rwa neg_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
541
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
542 lemma neg_pos : 0 < -a ↔ a < 0 :=
id ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴
543 have -0 < -a ↔ a < 0, from neg_lt_neg_iff,
id ┴ ┴ ┴┴ ┴ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴ ┴ ┴┴ ┴ ┴ ┴ └────────────┘
544 by rwa neg_zero at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
545
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
546 lemma neg_lt : -a < b ↔ -b < a :=
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
547 have -a < -(-b) ↔ -b < a, from neg_lt_neg_iff,
id ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ └────────────┘
548 by rwa neg_neg at this
id └─────┘
src └──┘└─────┘└────────
typ └──┘└─────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────
549
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
550 lemma lt_neg : a < -b ↔ b < -a :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴
551 have -(-a) < -b ↔ b < -a, from neg_lt_neg_iff,
id ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └────────────┘
552 by rwa neg_neg at this
id └─────┘
src └──┘└─────┘└────────
typ └──┘└─────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────
553
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
554 lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
555 (add_le_add_iff_left _).trans neg_le_neg_iff
id └─────────────────┘ └───┘ └────────────┘
src └─────────────────┘ └───┘ └────────────┘
typ └─────────────────┘ └───┘ └────────────┘
556
557 lemma sub_le_sub_iff_right (c : α) : a - c ≤ b - c ↔ a ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
558 add_le_add_iff_right _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
559
560 lemma sub_lt_sub_iff_left (a : α) {b c : α} : a - b < a - c ↔ c < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
561 (add_lt_add_iff_left _).trans neg_lt_neg_iff
id └─────────────────┘ └───┘ └────────────┘
src └─────────────────┘ └───┘ └────────────┘
typ └─────────────────┘ └───┘ └────────────┘
562
563 lemma sub_lt_sub_iff_right (c : α) : a - c < b - c ↔ a < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
564 add_lt_add_iff_right _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
565
566 @[simp] lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
567 have a - a ≤ a - b ↔ b ≤ a, from sub_le_sub_iff_left a,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
568 by rwa sub_self at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
569
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
570 @[simp] lemma sub_nonpos : a - b ≤ 0 ↔ a ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
571 have a - b ≤ b - b ↔ a ≤ b, from sub_le_sub_iff_right b,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └──────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴
572 by rwa sub_self at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
573
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
574 @[simp] lemma sub_pos : 0 < a - b ↔ b < a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
575 have a - a < a - b ↔ b < a, from sub_lt_sub_iff_left a,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
576 by rwa sub_self at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
577
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
578 @[simp] lemma sub_lt_zero : a - b < 0 ↔ a < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
579 have a - b < b - b ↔ a < b, from sub_lt_sub_iff_right b,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └──────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴
580 by rwa sub_self at this
id └──────┘
src └──┘└──────┘└────────
typ └──┘└──────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └─────────────────────
581
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
582 lemma le_neg_add_iff_add_le : b ≤ -a + c ↔ a + b ≤ c :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
583 have -a + (a + b) ≤ -a + c ↔ a + b ≤ c, from add_le_add_iff_left _,
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
584 by rwa neg_add_cancel_left at this
id └─────────────────┘
src └──┘└─────────────────┘└────────
typ └──┘└─────────────────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────────────────
585
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
586 lemma le_sub_iff_add_le' : b ≤ c - a ↔ a + b ≤ c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
587 by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
id └────────────┘ └──────┘ └───────────────────┘
src └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────────────┘└────────┘└─────────────────────┘┴└
588
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
589 lemma le_sub_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
590 by rw [le_sub_iff_add_le', add_comm]
id └────────────────┘ └──────┘
src └──┘└────────────────┘└┘└──────┘└─
typ └──┘└────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────────────┘└────────┘┴└
591
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
592 @[simp] lemma neg_add_le_iff_le_add : -b + a ≤ c ↔ a ≤ b + c :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
593 have -b + a ≤ -b + (b + c) ↔ a ≤ b + c, from add_le_add_iff_left _,
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
594 by rwa neg_add_cancel_left at this
id └─────────────────┘
src └──┘└─────────────────┘└────────
typ └──┘└─────────────────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────────────────
595
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
596 lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
597 by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add]
id └────────────┘ └──────┘ └───────────────────┘
src └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────────────┘└────────┘└─────────────────────┘┴└
598
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
599 lemma sub_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
600 by rw [sub_le_iff_le_add', add_comm]
id └────────────────┘ └──────┘
src └──┘└────────────────┘└┘└──────┘└─
typ └──┘└────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────────────┘└────────┘┴└
601
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
602 @[simp] lemma add_neg_le_iff_le_add : a + -c ≤ b ↔ a ≤ b + c :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
603 sub_le_iff_le_add
id └───────────────┘
src └───────────────┘
typ └───────────────┘
604
605 @[simp] lemma add_neg_le_iff_le_add' : a + -b ≤ c ↔ a ≤ b + c :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
606 sub_le_iff_le_add'
id └────────────────┘
src └────────────────┘
typ └────────────────┘
607
608 lemma neg_add_le_iff_le_add' : -c + a ≤ b ↔ a ≤ b + c :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
609 by rw [neg_add_le_iff_le_add, add_comm]
id └───────────────────┘ └──────┘
src └──┘└───────────────────┘└┘└──────┘└─
typ └──┘└───────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────────┘└────────┘┴└
610
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
611 @[simp] lemma neg_le_sub_iff_le_add : -b ≤ a - c ↔ c ≤ a + b :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
612 le_sub_iff_add_le.trans neg_add_le_iff_le_add'
id └───────────────┘└────┘ └────────────────────┘
src └───────────────┘└────┘ └────────────────────┘
typ └───────────────┘└────┘ └────────────────────┘
613
614 lemma neg_le_sub_iff_le_add' : -a ≤ b - c ↔ c ≤ a + b :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
615 by rw [neg_le_sub_iff_le_add, add_comm]
id └───────────────────┘ └──────┘
src └──┘└───────────────────┘└┘└──────┘└─
typ └──┘└───────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────────┘└────────┘┴└
616
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
617 lemma sub_le : a - b ≤ c ↔ a - c ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
618 sub_le_iff_le_add'.trans sub_le_iff_le_add.symm
id └────────────────┘└────┘ └───────────────┘└───┘
src └────────────────┘└────┘ └───────────────┘└───┘
typ └────────────────┘└────┘ └───────────────┘└───┘
619
620 theorem le_sub : a ≤ b - c ↔ c ≤ b - a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
621 le_sub_iff_add_le'.trans le_sub_iff_add_le.symm
id └────────────────┘└────┘ └───────────────┘└───┘
src └────────────────┘└────┘ └───────────────┘└───┘
typ └────────────────┘└────┘ └───────────────┘└───┘
622
623 @[simp] lemma lt_neg_add_iff_add_lt : b < -a + c ↔ a + b < c :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
624 have -a + (a + b) < -a + c ↔ a + b < c, from add_lt_add_iff_left _,
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
625 by rwa neg_add_cancel_left at this
id └─────────────────┘
src └──┘└─────────────────┘└────────
typ └──┘└─────────────────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────────────────
626
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
627 lemma lt_sub_iff_add_lt' : b < c - a ↔ a + b < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
628 by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt]
id └────────────┘ └──────┘ └───────────────────┘
src └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────────────┘└────────┘└─────────────────────┘┴└
629
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
630 lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
631 by rw [lt_sub_iff_add_lt', add_comm]
id └────────────────┘ └──────┘
src └──┘└────────────────┘└┘└──────┘└─
typ └──┘└────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────────────┘└────────┘┴└
632
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
633 @[simp] lemma neg_add_lt_iff_lt_add : -b + a < c ↔ a < b + c :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
634 have -b + a < -b + (b + c) ↔ a < b + c, from add_lt_add_iff_left _,
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
635 by rwa neg_add_cancel_left at this
id └─────────────────┘
src └──┘└─────────────────┘└────────
typ └──┘└─────────────────┘└────────
doc └──┘ └────────
txt └──┘ └────────
par └──┘ └────────
pid ┴ └──────┘└
st └────────────────────────────────
636
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
637 lemma sub_lt_iff_lt_add' : a - b < c ↔ a < b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
638 by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add]
id └────────────┘ └──────┘ └───────────────────┘
src └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────────────┘└────────┘└─────────────────────┘┴└
639
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
640 lemma sub_lt_iff_lt_add : a - c < b ↔ a < b + c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
641 by rw [sub_lt_iff_lt_add', add_comm]
id └────────────────┘ └──────┘
src └──┘└────────────────┘└┘└──────┘└─
typ └──┘└────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────────────┘└────────┘┴└
642
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
643 lemma neg_add_lt_iff_lt_add_right : -c + a < b ↔ a < b + c :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
644 by rw [neg_add_lt_iff_lt_add, add_comm]
id └───────────────────┘ └──────┘
src └──┘└───────────────────┘└┘└──────┘└─
typ └──┘└───────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────────┘└────────┘┴└
645
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
646 @[simp] lemma neg_lt_sub_iff_lt_add : -b < a - c ↔ c < a + b :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
647 lt_sub_iff_add_lt.trans neg_add_lt_iff_lt_add_right
id └───────────────┘└────┘ └─────────────────────────┘
src └───────────────┘└────┘ └─────────────────────────┘
typ └───────────────┘└────┘ └─────────────────────────┘
648
649 lemma neg_lt_sub_iff_lt_add' : -a < b - c ↔ c < a + b :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
650 by rw [neg_lt_sub_iff_lt_add, add_comm]
id └───────────────────┘ └──────┘
src └──┘└───────────────────┘└┘└──────┘└─
typ └──┘└───────────────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────────┘└────────┘┴└
651
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
652 lemma sub_lt : a - b < c ↔ a - c < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
653 sub_lt_iff_lt_add'.trans sub_lt_iff_lt_add.symm
id └────────────────┘└────┘ └───────────────┘└───┘
src └────────────────┘└────┘ └───────────────┘└───┘
typ └────────────────┘└────┘ └───────────────┘└───┘
654
655 theorem lt_sub : a < b - c ↔ c < b - a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
656 lt_sub_iff_add_lt'.trans lt_sub_iff_add_lt.symm
id └────────────────┘└────┘ └───────────────┘└───┘
src └────────────────┘└────┘ └───────────────┘└───┘
typ └────────────────┘└────┘ └───────────────┘└───┘
657
658 lemma sub_le_self_iff (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
659 sub_le_iff_le_add'.trans (le_add_iff_nonneg_left _)
id └────────────────┘└────┘ └────────────────────┘
src └────────────────┘└────┘ └────────────────────┘
typ └────────────────┘└────┘ └────────────────────┘
660
661 lemma sub_lt_self_iff (a : α) {b : α} : a - b < a ↔ 0 < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
662 sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _)
id └────────────────┘└────┘ └─────────────────┘
src └────────────────┘└────┘ └─────────────────┘
typ └────────────────┘└────┘ └─────────────────┘
663
664 end ordered_comm_group
665
666 namespace decidable_linear_ordered_comm_group
667 variables [s : decidable_linear_ordered_comm_group α]
id └─────────────────────────────────┘
src └─────────────────────────────────┘
typ └─────────────────────────────────┘
668 include s
669
670 @[priority 100] -- see Note [lower instance priority]
671 instance : decidable_linear_ordered_cancel_comm_monoid α :=
id └─────────────────────────────────────────┘ ┴
src └─────────────────────────────────────────┘
typ └─────────────────────────────────────────┘ ┴
672 { le_of_add_le_add_left := λ x y z, le_of_add_le_add_left,
id ┴ ┴ ┴ └───────────────────┘
src └───────────────────┘
typ ┴ ┴ ┴ └───────────────────┘
673 add_left_cancel := λ x y z, add_left_cancel,
id ┴ ┴ ┴ └─────────────┘
src └─────────────┘
typ ┴ ┴ ┴ └─────────────┘
674 add_right_cancel := λ x y z, add_right_cancel,
id ┴ ┴ ┴ └──────────────┘
src └──────────────┘
typ ┴ ┴ ┴ └──────────────┘
675 ..s }
id ┴
typ ┴
676
677 lemma eq_of_abs_sub_nonpos {a b : α} (h : abs (a - b) ≤ 0) : a = b :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
678 eq_of_abs_sub_eq_zero (le_antisymm _ _ h (abs_nonneg (a - b)))
id └───────────────────┘ └─────────┘ ┴ └────────┘ ┴ ┴ ┴
src └───────────────────┘ └─────────┘ └────────┘ ┴
typ └───────────────────┘ └─────────┘ ┴ └────────┘ ┴ ┴ ┴
679
680 end decidable_linear_ordered_comm_group
681
682 set_option old_structure_cmd true
doc └───────────────┘
683 section prio
684 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
685 /-- This is not so much a new structure as a construction mechanism
686 for ordered groups, by specifying only the "positive cone" of the group. -/
687 class nonneg_comm_group (α : Type*) extends add_comm_group α :=
id ┴ └───┘ └────────────┘ ┴
src └────────────┘
typ ┴ └───┘ └────────────┘ ┴
688 (nonneg : α → Prop)
id ┴ ┴
typ ┴ ┴
689 (pos : α → Prop := λ a, nonneg a ∧ ¬ nonneg (neg a))
id ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ └─┘ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ └─┘ ┴
690 (pos_iff : ∀ a, pos a ↔ nonneg a ∧ ¬ nonneg (-a) . order_laws_tac)
id ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴┴
doc ┴
691 (zero_nonneg : nonneg 0)
id └────┘
typ └────┘
692 (add_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a + b))
id ┴┴ ┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
src ┴ ┴
typ ┴┴ ┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
693 (nonneg_antisymm : ∀ {a}, nonneg a → nonneg (-a) → a = 0)
id ┴┴ └────┘ ┴ └────┘ ┴┴ ┴ ┴
src ┴ ┴
typ ┴┴ └────┘ ┴ └────┘ ┴┴ ┴ ┴
694 end prio
695
696 namespace nonneg_comm_group
697 variable [s : nonneg_comm_group α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
698 include s
699
700 @[reducible, priority 100] -- see Note [lower instance priority]
doc └───────┘
701 instance to_ordered_comm_group : ordered_comm_group α :=
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
702 { le := λ a b, nonneg (b - a),
id ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ ┴
703 lt := λ a b, pos (b - a),
id ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴
704 lt_iff_le_not_le := λ a b, by simp; rw [pos_iff]; simp,
id ┴ ┴ └─────┘
src └──┘ └──┘└─────┘┴ └──┘
typ ┴ ┴ └──┘ └──┘└─────┘┴ └──┘
doc └──┘ └──┘ ┴ └──┘
txt └──┘ └──┘ ┴ └──┘
par └──┘ └──┘ ┴ └──┘
pid └┘ ┴
st └─────────┘└─────┘┴└────┘
705 le_refl := λ a, by simp [zero_nonneg],
id ┴ └─────────┘
src └────┘└─────────┘┴
typ ┴ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────┘
706 le_trans := λ a b c nab nbc, by simp [-sub_eq_add_neg];
id ┴ ┴ ┴ └─┘ └─┘
src └────────────────────┘
typ ┴ ┴ ┴ └─┘ └─┘ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid ┴└───────────────┘
st └────────────────────────
707 rw ← sub_add_sub_cancel; exact add_nonneg nbc nab,
id └────────────────┘ └────────┘ └─┘ └─┘
src └───┘└────────────────┘ └────┘└────────┘┴ ┴
typ └───┘└────────────────┘ └────┘└────────┘┴└─┘┴└─┘
doc └───┘ └────┘ ┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid └─┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────┘
708 le_antisymm := λ a b nab nba, eq_of_sub_eq_zero $
id ┴ ┴ └─┘ └─┘ └───────────────┘
src └───────────────┘
typ ┴ ┴ └─┘ └─┘ └───────────────┘
709 nonneg_antisymm nba (by rw neg_sub; exact nab),
id └─────────────┘ └─┘ └─────┘ └─┘
src └─────────────┘ └─┘└─────┘ └────┘
typ └─────────────┘ └─┘ └─┘└─────┘ └────┘└─┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └────────────────────┘
710 add_le_add_left := λ a b nab c, by simpa [(≤), preorder.le] using nab,
id ┴ ┴ └─┘ ┴ └─┘
src └─────┘ └──┘ └──────┘
typ ┴ ┴ └─┘ ┴ └─────┘ └──┘ └──────┘└─┘
doc └─────┘ └──┘ └──────┘
txt └─────┘ └──┘ └──────┘
par └─────┘ └──┘ └──────┘
pid ┴┴ └──┘ ┴┴└────┘
st └─────────────────────────────────┘
711 add_lt_add_left := λ a b nab c, by simpa [(<), preorder.lt] using nab, ..s }
id ┴ ┴ └─┘ ┴ └─┘ ┴
src └─────┘ └──┘ └──────┘
typ ┴ ┴ └─┘ ┴ └─────┘ └──┘ └──────┘└─┘ ┴
doc └─────┘ └──┘ └──────┘
txt └─────┘ └──┘ └──────┘
par └─────┘ └──┘ └──────┘
pid ┴┴ └──┘ ┴┴└────┘
st └─────────────────────────────────┘
712
713 theorem nonneg_def {a : α} : nonneg a ↔ 0 ≤ a :=
id ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴
714 show _ ↔ nonneg _, by simp
id ┴ └────┘
src ┴ └────┘ └────
typ ┴ └────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
715
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
716 theorem pos_def {a : α} : pos a ↔ 0 < a :=
id ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴
717 show _ ↔ pos _, by simp
id ┴ └─┘
src ┴ └─┘ └────
typ ┴ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
718
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
719 theorem not_zero_pos : ¬ pos (0 : α) :=
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
720 mt pos_def.1 (lt_irrefl _)
id └┘ └─────┘┴ └───────┘
src └┘ └─────┘┴ └───────┘
typ └┘ └─────┘┴ └───────┘
721
722 theorem zero_lt_iff_nonneg_nonneg {a : α} :
id ┴
typ ┴
723 0 < a ↔ nonneg a ∧ ¬ nonneg (-a) :=
id ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴┴
src ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
typ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴┴
724 pos_def.symm.trans (pos_iff α _)
id └─────┘└───┘└────┘ └─────┘ ┴
src └─────┘└───┘└────┘ └─────┘
typ └─────┘└───┘└────┘ └─────┘ ┴
725
726 theorem nonneg_total_iff :
727 (∀ a : α, nonneg a ∨ nonneg (-a)) ↔
id ┴ └────┘ ┴ ┴ └────┘ ┴┴ ┴
src └────┘ ┴ └────┘ ┴ ┴
typ ┴ └────┘ ┴ ┴ └────┘ ┴┴ ┴
728 (∀ a b : α, a ≤ b ∨ b ≤ a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
729 ⟨λ h a b, by have := h (b - a); rwa [neg_sub] at this,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └──────┘ ┴ ┴┴┴ ┴ └───┘└─────┘└───────┘
typ ┴ ┴ ┴ └──────┘┴┴ ┴┴┴┴┴┴ └───┘└─────┘└───────┘
doc └──────┘ ┴ ┴ ┴ ┴ └───┘ └───────┘
txt └──────┘ ┴ ┴ ┴ ┴ └───┘ └───────┘
par └──────┘ ┴ ┴ ┴ ┴ └───┘ └───────┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴└──────┘
st └───────────────────────┘└─────┘┴└──────┘
730 λ h a, by rw [nonneg_def, nonneg_def, neg_nonneg]; apply h⟩
id ┴ ┴ └────────┘ └────────┘ └────────┘
src └──┘└────────┘└┘└────────┘└┘└────────┘┴ └────┘
typ ┴ ┴ └──┘└────────┘└┘└────────┘└┘└────────┘┴ └────┘
doc └──┘ └┘ └┘ ┴ └────┘
txt └──┘ └┘ └┘ ┴ └────┘
par └──┘ └┘ └┘ ┴ └────┘
pid └┘ └┘ └┘ ┴ ┴
st └─────────────┘└──────────┘└──────────┘┴└───────┘
731
732 def to_decidable_linear_ordered_comm_group
733 [decidable_pred (@nonneg α _)]
id └────────────┘ └────┘ ┴
src └────────────┘ └────┘
typ └────────────┘ └────┘ ┴
734 (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
id ┴ └────┘ ┴ ┴ └────┘ ┴┴
src └────┘ ┴ └────┘ ┴
typ ┴ └────┘ ┴ ┴ └────┘ ┴┴
735 : decidable_linear_ordered_comm_group α :=
id └─────────────────────────────────┘ ┴
src └─────────────────────────────────┘
typ └─────────────────────────────────┘ ┴
736 { le := (≤),
id ┴
src ┴
typ ┴
737 lt := (<),
id ┴
src ┴
typ ┴
738 lt_iff_le_not_le := @lt_iff_le_not_le _ _,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
739 le_refl := @le_refl _ _,
id └─────┘
src └─────┘
typ └─────┘
740 le_trans := @le_trans _ _,
id └──────┘
src └──────┘
typ └──────┘
st ┴
741 le_antisymm := @le_antisymm _ _,
id └─────────┘
src └─────────┘
typ └─────────┘
742 le_total := nonneg_total_iff.1 nonneg_total,
id └──────────────┘┴ └──────────┘
src └──────────────┘┴
typ └──────────────┘┴ └──────────┘
743 decidable_le := by apply_instance,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
744 decidable_eq := by apply_instance,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
745 decidable_lt := by apply_instance,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
746 ..@nonneg_comm_group.to_ordered_comm_group _ s }
id └─────────────────────────────────────┘ ┴
src └─────────────────────────────────────┘
typ └─────────────────────────────────────┘ ┴
747
748 end nonneg_comm_group
749
750 namespace order_dual
751
752 instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
id └─────────────────┘ ┴ └─────────────────┘ └────────┘ ┴
src └─────────────────┘ └─────────────────┘ └────────┘
typ └─────────────────┘ ┴ └─────────────────┘ └────────┘ ┴
doc └─────────────────┘ └─────────────────┘ └────────┘
753 { add_le_add_left := λ a b h c, @add_le_add_left' α _ b a c h,
id ┴ ┴ ┴ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────────┘
typ ┴ ┴ ┴ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴
754 lt_of_add_lt_add_left := λ a b c h, @lt_of_add_lt_add_left' α _ a c b h,
id ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘
typ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
755 ..order_dual.partial_order α,
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
756 ..show add_comm_monoid α, by apply_instance }
id └─────────────┘ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
757
758 instance [ordered_cancel_comm_monoid α] : ordered_cancel_comm_monoid (order_dual α) :=
id └────────────────────────┘ ┴ └────────────────────────┘ └────────┘ ┴
src └────────────────────────┘ └────────────────────────┘ └────────┘
typ └────────────────────────┘ ┴ └────────────────────────┘ └────────┘ ┴
doc └────────┘
759 { le_of_add_le_add_left := λ a b c : α, le_of_add_le_add_left,
id ┴ └───────────────────┘
src └───────────────────┘
typ ┴ └───────────────────┘
760 add_left_cancel := @add_left_cancel α _,
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
761 add_right_cancel := @add_right_cancel α _,
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
762 ..order_dual.ordered_comm_monoid }
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
763
764 instance [ordered_comm_group α] : ordered_comm_group (order_dual α) :=
id └────────────────┘ ┴ └────────────────┘ └────────┘ ┴
src └────────────────┘ └────────────────┘ └────────┘
typ └────────────────┘ ┴ └────────────────┘ └────────┘ ┴
doc └────────┘
765 { add_lt_add_left := λ a b : α, ordered_comm_group.add_lt_add_left b a,
id ┴ └────────────────────────────────┘ ┴ ┴
src └────────────────────────────────┘
typ ┴ └────────────────────────────────┘ ┴ ┴
766 add_left_neg := λ a : α, add_left_neg a,
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
767 ..order_dual.ordered_comm_monoid,
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
768 ..show add_comm_group α, by apply_instance }
id └────────────┘ ┴
src └────────────┘ └─────────────┘
typ └────────────┘ ┴ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
769
770 end order_dual